Verification, model checking, and abstract interpretation

InhaltsverzeichnisInvited 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.