Gogul Balakrishnan, Thomas Reps (auth.), Byron Cook, Andreas Podelski (eds.)3540697357, 9783540697350
Table of contents :
Front Matter….Pages –
DIVINE: DIscovering Variables IN Executables….Pages 1-28
Verifying Compensating Transactions….Pages 29-43
Model Checking Nonblocking MPI Programs….Pages 44-58
Model Checking Via ΓCFA….Pages 59-73
Using First-Order Theorem Provers in the Jahob Data Structure Verification System….Pages 74-88
Interpolants and Symbolic Model Checking….Pages 89-90
Shape Analysis of Single-Parent Heaps….Pages 91-105
An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures….Pages 106-121
On Flat Programs with Lists….Pages 122-136
Automata-Theoretic Model Checking Revisited….Pages 137-150
Language-Based Abstraction Refinement for Hybrid System Verification….Pages 151-166
More Precise Partition Abstractions….Pages 167-181
The Spotlight Principle….Pages 182-198
Lattice Automata….Pages 199-213
Learning Algorithms and Formal Verification (Invited Tutorial)….Pages 214-214
Constructing Specialized Shape Analyses for Uniform Change….Pages 215-233
Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning….Pages 234-250
Automated Verification of Shape and Size Properties Via Separation Logic….Pages 251-266
Towards Shape Analysis for Device Drivers….Pages 267-267
An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints….Pages 268-282
Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes….Pages 283-298
Symmetry and Completeness in the Analysis of Parameterized Systems….Pages 299-313
Better Under-Approximation of Programs by Hiding Variables….Pages 314-328
The Constraint Database Approach to Software Verification….Pages 329-345
Constraint Solving for Interpolation….Pages 346-362
Assertion Checking Unified….Pages 363-377
Invariant Synthesis for Combined Theories….Pages 378-394
Back Matter….Pages –
Reviews
There are no reviews yet.