LEADER 04082nam  22006255  450 
001 996465274003316
005 20230406033851.0
010   $a3-540-69738-1
024 7 $a10.1007/978-3-540-69738-1
035   $a(CKB)1000000000491071
035   $a(SSID)ssj0000320624
035   $a(PQKBManifestationID)11231124
035   $a(PQKBTitleCode)TC0000320624
035   $a(PQKBWorkID)10248720
035   $a(PQKB)11022152
035   $a(DE-He213)978-3-540-69738-1
035   $a(MiAaPQ)EBC3062815
035   $a(MiAaPQ)EBC6501291
035   $a(PPN)123726646
035   $a(EXLCZ)991000000000491071
100   $a20100301d2007      u|             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aVerification, Model Checking, and Abstract Interpretation$b[electronic resource] $e8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings /$fedited by Byron Cook, Andreas Podelski
205   $a1st ed. 2007.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2007.
215   $a1 online resource (XI, 395 p.) 
225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4349
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-69735-7 
320   $aIncludes bibliographical references and index.
327   $aInvited Talk -- DIVINE: DIscovering Variables IN Executables -- Session 1 -- Verifying Compensating Transactions -- Model Checking Nonblocking MPI Programs -- Model Checking Via ?CFA -- Using First-Order Theorem Provers in the Jahob Data Structure Verification System -- Invited Tutorial -- Interpolants and Symbolic Model Checking -- Session 2 -- Shape Analysis of Single-Parent Heaps -- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures -- On Flat Programs with Lists -- Invited Talk -- Automata-Theoretic Model Checking Revisited -- Session 3 -- Language-Based Abstraction Refinement for Hybrid System Verification -- More Precise Partition Abstractions -- The Spotlight Principle -- Lattice Automata -- Invited Tutorial -- Learning Algorithms and Formal Verification (Invited Tutorial) -- Session 4 -- Constructing Specialized Shape Analyses for Uniform Change -- Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning -- Automated Verification of Shape and Size Properties Via Separation Logic -- Invited Talk -- Towards Shape Analysis for Device Drivers -- Session 5 -- An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints -- Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes -- Symmetry and Completeness in the Analysis of Parameterized Systems -- Better Under-Approximation of Programs by Hiding Variables -- Invited Tutorial -- The Constraint Database Approach to Software Verification -- Session 6 -- Constraint Solving for Interpolation -- Assertion Checking Unified -- Invariant Synthesis for Combined Theories.
410  0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4349
606   $aSoftware engineering
606   $aComputer science
606   $aCompilers (Computer programs)
606   $aSoftware Engineering
606   $aComputer Science Logic and Foundations of Programming
606   $aCompilers and Interpreters
615  0$aSoftware engineering.
615  0$aComputer science.
615  0$aCompilers (Computer programs).
615 14$aSoftware Engineering.
615 24$aComputer Science Logic and Foundations of Programming.
615 24$aCompilers and Interpreters.
676   $a005.14
702   $aCook$b Byron$4edt$4http://id.loc.gov/vocabulary/relators/edt
702   $aPodelski$b Andreas$4edt$4http://id.loc.gov/vocabulary/relators/edt
906   $aBOOK
912   $a996465274003316
996   $aVerification, Model Checking, and Abstract Interpretation$92593983
997   $aUNISA