LEADER 05190nam  22008175  450 
001 996210523003316
005 20200705094048.0
010   $a3-319-13338-1
024 7 $a10.1007/978-3-319-13338-6
035   $a(CKB)3710000000306189
035   $a(SSID)ssj0001386526
035   $a(PQKBManifestationID)11817455
035   $a(PQKBTitleCode)TC0001386526
035   $a(PQKBWorkID)11374294
035   $a(PQKB)11148374
035   $a(DE-He213)978-3-319-13338-6
035   $a(MiAaPQ)EBC6300699
035   $a(MiAaPQ)EBC5586615
035   $a(Au-PeEL)EBL5586615
035   $a(OCoLC)1066199650
035   $a(PPN)183094700
035   $a(EXLCZ)993710000000306189
100   $a20141103d2014      u|             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aHardware and Software: Verification and Testing$b[electronic resource] $e10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings /$fedited by Eran Yahav
205   $a1st ed. 2014.
210  1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2014.
215   $a1 online resource (XVI, 302 p. 78 illus.) 
225 1 $aProgramming and Software Engineering ;$v8855
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-319-13337-3 
327   $aUsing Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures -- Enhancing Scenario Quality Using Quasi-Events -- Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems -- DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification -- Generating Modulo-2 Linear Invariants for Hardware Model Checking -- Suraq ? A Controller Synthesis Tool Using Uninterpreted Functions -- Synthesizing Finite-State Protocols from Scenarios and Requirements -- Automatic Error Localization for Software Using Deductive Verification -- Generating JML Specifications from Alloy Expressions -- Assume-Guarantee Abstraction Refinement Meets Hybrid Systems -- Handling TSO in Mechanized Linearizability Proofs -- Partial Quantifier Elimination -- Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study -- A Framework to Synergize Partial Order Reduction with State Interpolation -- Reduction of Resolution Refutations and Interpolants via Subsumption -- Read, Write and Copy Dependencies for Symbolic Model Checking -- Efficient Combinatorial Test Generation Based on Multivalued Decision Diagrams -- Formal Verification of Secure User Mode Device Execution with DMA -- Supervisory Control of Discrete-Event Systems via IC3 -- Partial-Order Reduction for Multi-core LTL Model Checking -- A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution.
330   $aThis book constitutes the refereed proceedings of the 10th International Haifa Verification Conference, HVC 2014, held in Haifa, Israel, in November 2014. The 17 revised full papers and 4 short papers presented were carefully reviewed and selected from 43 submissions. The papers cover a wide range of topics in the sub-fields of testing and verification applicable to software, hardware, and complex hybrid systems.
410  0$aProgramming and Software Engineering ;$v8855
606   $aSoftware engineering
606   $aComputer logic
606   $aProgramming languages (Electronic computers)
606   $aArtificial intelligence
606   $aMathematical logic
606   $aComputer communication systems
606   $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029
606   $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X
606   $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037
606   $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000
606   $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048
606   $aComputer Communication Networks$3https://scigraph.springernature.com/ontologies/product-market-codes/I13022
615  0$aSoftware engineering.
615  0$aComputer logic.
615  0$aProgramming languages (Electronic computers).
615  0$aArtificial intelligence.
615  0$aMathematical logic.
615  0$aComputer communication systems.
615 14$aSoftware Engineering.
615 24$aLogics and Meanings of Programs.
615 24$aProgramming Languages, Compilers, Interpreters.
615 24$aArtificial Intelligence.
615 24$aMathematical Logic and Formal Languages.
615 24$aComputer Communication Networks.
676   $a005.14
702   $aYahav$b Eran$4edt$4http://id.loc.gov/vocabulary/relators/edt
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a996210523003316
996   $aHardware and Software, Verification and Testing$9772242
997   $aUNISA