Computer Aided Verification: 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, ProceedingsAarti Gupta, Sharad Malik This book constitutes the refereed proceedings of the 20th International Conference on Computer Aided Verification, CAV 2008, held in Princeton, NJ, USA, in July 2008. The 33 revised full papers presented together with 14 tool papers and 2 invited papers and 4 invited tutorials were carefully reviewed and selected from 104 regular paper and 27 tool paper submissions. The papers are organized in topical sections on concurrency, memory consistency, abstraction/refinement, hybrid systems, dynamic verification, modeling and specification formalisms, decision procedures, program verification, program and shape analysis, security and program analysis, hardware verification, model checking, space efficient algorithms, and model checking. |
Contents
| 1 | |
| 3 | |
| 5 | |
| 11 | |
Tutorial on Separation Logic | 19 |
Abstract Interpretation with Applications to Timing Validation | 22 |
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis | 37 |
Monitoring Atomicity in Concurrent Programs | 52 |
Interpolation for LA+EUF | 304 |
A UserCentric Approach to Verification with Isabelle and QEPCADB | 309 |
Heap Assumptions on Demand | 314 |
Proving Conditional Termination | 328 |
Monotonic Abstraction for Programs with Dynamic Memory Heaps | 341 |
Enhancing Program Verification with Lemmas | 355 |
A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis | 370 |
Scalable Shape Analysis for Systems Code | 385 |
Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings | 66 |
A Hybrid Type System for LockFreedom of Mobile Processes | 80 |
Implied Set Closure and Its Application to Memory Consistency Verification | 94 |
Effective Program Verification for Relaxed Memory Models | 107 |
Mechanical Verification of Transactional Memories with Nontransactional Memory Accesses | 121 |
Automated AssumeGuarantee Reasoning by Abstraction Refinement | 135 |
Local Proofs for LinearTime Properties of Concurrent Programs | 149 |
Probabilistic CEGAR | 162 |
Computing Differential Invariants of Hybrid Systems as Fixedpoints | 176 |
ConstraintBased Approach for Analysis of Hybrid Systems | 190 |
Automatic Model Oriented Test Generator for Embedded Control Systems | 204 |
Systematic Test Case Generation for Dynamic Analysis and Measurement | 209 |
Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems | 214 |
ConflictTolerant Features | 227 |
Ranking Automata and Gamesfor Prioritized Requirements | 240 |
Efficient Craig Interpolation for Linear Diophantine DisEquations and Linear Modular Equations | 254 |
Linear Arithmetic with Stars | 268 |
Inferring Congruence Equations Using SAT | 281 |
The Barcelogic SMT Solver | 294 |
The MathSAT 4 SMT Solver | 299 |
Thread Quantification for Concurrent Shape Analysis | 399 |
Verification Falsification and Analysis of Security Protocols | 414 |
CausalityBased Abstraction for Security Protocol Analysis | 419 |
A Static Analysis Platform for Binaries | 423 |
A Tool for Reasoning about Shape and Arithmetic | 428 |
Functional Verification of Power Gated Designs by Compositional Reasoning | 433 |
A Practical Approach to Word Level Model Checking of Industrial Netlists | 446 |
Validating HighLevel Synthesis | 459 |
An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths | 473 |
Application of FormalWordLevel Analysis to Constrained Random Simulation | 487 |
Producing Short Counterexamples Using Crucial Events | 491 |
Discriminative Model Checking | 504 |
Correcting a SpaceEfficient Simulation Algorithm | 517 |
Semiexternal LTL Model Checking | 530 |
A Model Checker for Quantum Systems | 543 |
A Tool for ωRegular Model Checking | 548 |
Faster Than UPPAAL ? | 552 |
| 556 | |
Common terms and phrases
abstract domain abstract interpretation algorithm applied approach arithmetic automated automatically automaton Berlin Heidelberg 2008 bisimulation Boolean bound Büchi Büchi automaton cache checker compute concurrent programs condition conflict graph conflict-tolerant constraints counterexample data structures defined denote equations equivalence example execution expressions finite formal formal verification formula global graph Gröbner basis heap hybrid systems IEEE implementation input integer interpolant invariants iteration Lemma linear LNCS lock-freedom loop Malik Eds memory model checking morphisms multisets netlist nodes operations output partition pair path polynomial precondition predicate problem procedure proof protocol prove pushout QFPA quantified reachable reduction refinement satisfies schedule Scyther Section semantics sequence sequential serializability shape analysis simulation solver specification Springer system of LDEs techniques temporal logic termination Theorem thread tion tool transaction transition relation type system update variables vector verification vertex word-level