Verification, Model Checking, and Abstract Interpretation: 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings (Lecture Notes in Computer Science, 4349)

The book constitutes the refereed proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007, held in Nice, France in January 2007. This event was co-located with the Symposium on Principles of Programming Languages (POPL 2007). The 21 revised full papers presented together with three invited lectures and three invited tutorials were carefully reviewed and selected from a total of 85 submissions. DIVINE: DIscovering Variables IN Executables Introduction An Abstract Memory Model Overview of Our Approach The Problem of Indirect Memory Accesses The Problem of Granularity and Expressiveness Background Value-Set Analysis (VSA) Aggregate Structure Identification (ASI) Recovering A-Locs Via Iteration Generating Data-Access Constraints Interpreting Indirect Memory-References Hierarchical A-Locs Convergence Pragmatics Experiments Comparison of A-Locs with Program Variables Usefulness of the A-Locs for Static Analysis Related Work Verifying Compensating Transactions Introduction Sagas with Compensation Trace Semantics Tree Semantics Yield Language of a Saga Tree Automata with One Memory Verification in the Tree Semantics Conclusions and Future Work Model Checking Nonblocking MPI Programs Introduction Nonblocking Communication Modeling Approach Communication Records Local Process Model Global Model Order Validation Model Checking Via ΓCFA Introduction CPS Generating the Abstract State Graph with $\rm \Gamma$CFA Governors Conditional Abstract Garbage Collection Termination A Small Example A Higher-Order Example Understanding Abstract Garbage Collection Implementation Related Work Using First-Order Theorem Provers in the Jahob Data Structure Verification System Introduction Binary Tree Example Translation to First-Order Logic From Multisorted to Unsorted Logic Experimental Results Related Work Interpolants and Symbolic Model Checking Introduction Shape Analysis of Single-Parent Heaps Introduction The Formal Framework Fair Discrete Systems Predicate Abstraction Single-Parent Heaps Computing Symbolic Abstractions of Single-Parent Heaps Multi-linked Heap Systems Reducing Multi-linked into Single-Parent Heaps The Transformation Correctness of Transformation Conclusion An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures Introduction Review of Our Previous Logic and Decision Procedure New Extensions to Logic and Decision Procedure Mutable Data Fields Cyclicity Multiple Pointer Fields Correctness of the Decision Procedure Experimental Results Future Work and Conclusions Inference Rules from Previous Work bingham2006,bingham-rakamaric-tr2005-19 On Flat Programs with Lists Introduction Related Work Preliminaries Programs with Lists Arithmetic of Integers Counter Automata Undecidable Flat List Programs Extensions of the Undecidability Results Decidability on Acyclic and 1-Cyclic Heaps From List Programs to Counter Automata Reasoning About Counter Automata Conclusions Automata-Theoretic Model Checking Revisited Introduction Basic Theory Automata-Theoretic Model Checking Revisited Translating LTL Formulas to Büchi Automata Deterministic vs. Nondeterministic Automata Nonemptiness Algorithms Büchi Properties Concluding Remarks Language-Based Abstraction Refinement for Hybrid System Verification Introduction Verification of Hybrid Systems Language-Based Abstractions Region Pruning Incremental Computation Language Representation and Manipulation Counterexample Checking Experimental Results Conclusion More Precise Partition Abstractions Introduction Preliminaries Partition-Induced Satisfaction Games Precise Abstractions for Pre-satisfaction Precise Abstractions for Post-satisfaction Automated Synthesis of Precise Abstractions Expressiveness of Pre- and Post-abstractions Abstraction Refinement Discussion Conclusions The Spotlight Principle Introduction Computational Model and Property Specification Parameterised Systems Properties Augmentation Defining and Comparing State Abstractions Comparing State Abstractions Canonical Abstraction The Spotlight Principle Data-Type Reduction Environment Abstraction Shape Analysis Combining DTR and EA Conclusion Lattice Automata Introduction Preliminaries Lattices Lattice Automata Closure Properties Nondeterministic Automata on Finite Words Deterministic Automata on Finite Words Lattice Automata on Infinite Words Applications Decision Problems LLTL Model Checking and Satisfiability Learning Algorithms and Formal Verification Introduction Overview Preliminaries Programming-Language Statements Monadic-Uniform Updates Canonical Abstraction Methodology for Developing Computable Transformers Applications Related Work Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning Introduction Background: Local Analysis of Single Heap Cells Example Reference Counts and DLL Invariants Maintaining the DLL Invariant Using Local Reasoning The Local Abstraction Analysis of the Example Analysis Algorithm Assume-and-Check Approach Soundness Evaluation Related Work Conclusions Automated Verification of Shape and Size Properties Via Separation Logic Introduction User-Definable Shape Predicates Automated Verification Language Forward Verification Forward Verification Example Entailment Separation Constraint Approximation Separation Constraint Entailment Unfold/Fold Mechanism Unfolding a Shape Predicate in the Antecedent Folding a Shape Predicate in the Consequent Soundness of Entailment Implementation Related Work Conclusion Towards Shape Analysis for Device Drivers Introduction Related Works Difference-Bound Matrices \cite{Di89} Extending DBMs Emptiness Test and Normal Form The Dense Case The Arithmetic Case Operators on dDBMs The Lattice of dDBMs Other Operators Application to Program Analysis Conclusion Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes Introduction Preliminaries Abstract Domains Abstract Environment Abstract Store Abstract State The Analyzer Overall Structure Dynamic Octagon Operations Transfer Functions Experiments Related Work Conclusions and Future Work Symmetry and Completeness in the Analysis of Parameterized Systems Introduction Contributions Completeness of the Cutoff Method Completeness Parameterized Invariants and Non-interference Background Non-interference and Split Invariants Quantified Inductive Invariants Simple BDS's Experiments Related Work Better Under-Approximation of Programs by Hiding Variables Introduction Preliminaries Partitioned-Must Transitions Calculation of Partitioned-Must Transitions Applications Linear-Time Falsification A Multi-valued Semantics Choosing the Relevant Variables An Abstraction Based on $X$ Choosing $X$ The Constraint Database Approach to Software Verification Introduction Basic Concepts Constraints Abstract Interpretation Addition-Bound Matrices Operations on ABMs The l-u-Widening Operator Properties of l-u-Widening A Simple Program with Goto Statements The Subway Train Example Non-convex Invariants Verification An Efficient Representation of ABMs Related and Future Work Constraint Solving for Interpolation Introduction Preliminaries Linear Interpolants Interpolants for Disjunctions Extension with Uninterpreted Function Symbols A Hierarchical Calculus Hierarchical Interpolation in $LI({\mathbb Q})^{\Sigma}$ Experiments Conclusion and Ongoing Work Assertion Checking Unified Introduction Preliminaries Program Model Unification Terminology Connection Between Unification and Assertion Checking PTIME Decidability for Strict Unitary Theories Algorithm Examples of Strict Unitary Theories coNP-Hardness for Bitary Theories Reduction from 3-SAT Examples of Bitary Theories Decidability for Finitary Convex Theories Algorithm Examples of Finitary Convex Theory Discussion Conclusion Invariant Synthesis for Combined Theories Introduction Example Preliminaries Invariant Synthesis for LI+UIF Invariant Templates Algorithm Experiences Applications to Data Structures Conclusion The book constitutes the refereed proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007, held in Nice, France in January 2007, co-located with the Symposium on Principles of Programming Languages (POPL 2007). The 21 revised full papers presented together with 3 invited lectures and 3 invited tutorials were carefully reviewed and selected from a total of 85 submissions. The papers feature current research from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods