Verification, Model Checking, and Abstract Interpretation

Inhaltsverzeichnis

• 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.
• Automata-Theoretic Model Checking Revisited.
• Session 3.
• Language-Based Abstraction Refinement for Hybrid System Verification.
• More Precise Partition Abstractions.
• The Spotlight Principle.
• Lattice Automata.
• 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.
• 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.
• The Constraint Database Approach to Software Verification.
• Session 6.
• Constraint Solving for Interpolation.
• Assertion Checking Unified.
• Invariant Synthesis for Combined Theories.