04082nam 22006255 450 99646527400331620230406033851.03-540-69738-110.1007/978-3-540-69738-1(CKB)1000000000491071(SSID)ssj0000320624(PQKBManifestationID)11231124(PQKBTitleCode)TC0000320624(PQKBWorkID)10248720(PQKB)11022152(DE-He213)978-3-540-69738-1(MiAaPQ)EBC3062815(MiAaPQ)EBC6501291(PPN)123726646(EXLCZ)99100000000049107120100301d2007 u| 0engurnn|008mamaatxtccrVerification, Model Checking, and Abstract Interpretation[electronic resource] 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings /edited by Byron Cook, Andreas Podelski1st ed. 2007.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2007.1 online resource (XI, 395 p.) Theoretical Computer Science and General Issues,2512-2029 ;4349Bibliographic Level Mode of Issuance: Monograph3-540-69735-7 Includes bibliographical references and index.Invited 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.Theoretical Computer Science and General Issues,2512-2029 ;4349Software engineeringComputer scienceCompilers (Computer programs)Software EngineeringComputer Science Logic and Foundations of ProgrammingCompilers and InterpretersSoftware engineering.Computer science.Compilers (Computer programs).Software Engineering.Computer Science Logic and Foundations of Programming.Compilers and Interpreters.005.14Cook Byronedthttp://id.loc.gov/vocabulary/relators/edtPodelski Andreasedthttp://id.loc.gov/vocabulary/relators/edtBOOK996465274003316Verification, Model Checking, and Abstract Interpretation2593983UNISA