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

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 -