Verification, Model Checking, and Abstract Interpretation: Lecture Notes in Computer Science

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.