Computer Aided Verification: 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007. Proceedings

Byron Cook (auth.), Werner Damm, Holger Hermanns (eds.)3540733671, 9783540733676

This volume contains the proceedings of the International Conference on C- puter Aided Veri?cation (CAV), held in Berlin, Germany, July 3–7, 2007. CAV 2007 was the 19th in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical – sults to concrete applications, with an emphasis on practical veri?cation tools and the algorithms and techniques that are needed for their implementation. We received 134 regular paper submissions and 39 tool paper submissions. Of these, the ProgramCommittee selected 33 regularpapersand 14 toolpapers. Each submission was reviewed by at least three members of the Program C- mittee. The reviewing process included a PC review meeting, and – for the ?rst time in the history of CAV – an author feedback period. About 50 additional reviews were provided by experts external to the Program Committee to assure a high quality selection. The CAV 2007 program included three invited talks from industry: – Byron Cook (Microsoft Research) on Automatically Proving Program T- mination, – David Russino? (AMD) on A Mathematical Approach to RTL Veri?cation, and – Thomas Kropf (Bosch) on Software Bugs Seen from an Industrial Persp- tive.

---

Table of contents :
Front Matter….Pages –
Automatically Proving Program Termination….Pages 1-1
A Mathematical Approach to RTL Verification….Pages 2-2
Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development?….Pages 3-3
Algorithms for Interface Synthesis….Pages 4-19
A Tutorial on Satisfiability Modulo Theories….Pages 20-36
A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java….Pages 37-37
Verification of Hybrid Systems….Pages 38-38
SAT-Based Compositional Verification Using Lazy Learning….Pages 39-54
Local Proofs for Global Safety Properties….Pages 55-67
Low-Level Library Analysis and Summarization….Pages 68-81
Verification Across Intellectual Property Boundaries….Pages 82-94
On Synthesizing Controllers from Bounded-Response Properties….Pages 95-107
An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games….Pages 108-120
UPPAAL-Tiga: Time for Playing Games!….Pages 121-125
The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems….Pages 126-130
Systematic Acceleration in Regular Model Checking….Pages 131-144
Parameterized Verification of Infinite-State Processes with Global Conditions….Pages 145-157
CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes….Pages 158-163
jMoped: A Test Environment for Java Programs….Pages 164-167
Hector : Software Model Checking with Cooperating Analysis Plugins….Pages 168-172
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification….Pages 173-177
Shape Analysis for Composite Data Structures….Pages 178-192
Array Abstractions from Proofs….Pages 193-206
Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures….Pages 207-220
Revamping TVLA: Making Parametric Shape Analysis Competitive….Pages 221-225
Fast and Accurate Static Data-Race Detection for Concurrent Programs….Pages 226-239
Parametric and Sliced Causality….Pages 240-253
Spade : Verification of Multithreaded Dynamic and Recursive Programs….Pages 254-257
Anzu: A Tool for Property Synthesis….Pages 258-262
RAT: A Tool for the Formal Analysis of Requirements….Pages 263-267
Parallelising Symbolic State-Space Generators….Pages 268-280
I/O Efficient Accepting Cycle Detection….Pages 281-293
C32SAT: Checking C Expressions….Pages 294-297
CVC3….Pages 298-302
BAT: The Bit-Level Analysis Tool….Pages 303-306
LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals….Pages 307-310
Three-Valued Abstraction for Continuous-Time Markov Chains….Pages 311-324
Magnifying-Lens Abstraction for Markov Decision Processes….Pages 325-338
Underapproximation for Model-Checking Based on Random Cryptographic Constructions….Pages 339-351
Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra….Pages 352-365
Structural Abstraction of Software Verification Conditions….Pages 366-378
An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software….Pages 379-392
Adaptive Symmetry Reduction….Pages 393-405
From Liveness to Promptness….Pages 406-419
Automated Assumption Generation for Compositional Verification….Pages 420-432
Abstraction and Counterexample-Guided Construction of ω -Automata for Model Checking of Step-Discrete Linear Hybrid Models….Pages 433-448
Test Coverage for Continuous and Hybrid Systems….Pages 449-462
Hybrid Systems: From Verification to Falsification….Pages 463-476
Comparison Under Abstraction for Verifying Linearizability….Pages 477-490
Leaping Loops in the Presence of Abstraction….Pages 491-503
Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis….Pages 504-518
A Decision Procedure for Bit-Vectors and Arrays….Pages 519-531
Boolean Abstraction for Temporal Logic Satisfiability….Pages 532-546
A Lazy and Layered SMT( $mathcal{BV}$ ) Solver for Hard Industrial Verification Problems….Pages 547-560
Back Matter….Pages –