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.
Author(s): James R. Larus (auth.), Aarti Gupta, Sharad Malik (eds.)
Series: Lecture Notes in Computer Science 5123 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2008
Language: English
Pages: 558
Tags: Logics and Meanings of Programs; Software Engineering; Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Logic Design
Front Matter....Pages -
Singularity: Designing Better Software (Invited Talk)....Pages 1-2
Coping with Outside-the-Box Attacks....Pages 3-4
Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial)....Pages 5-10
Theorem Proving for Verification (Invited Tutorial)....Pages 11-18
Tutorial on Separation Logic (Invited Tutorial)....Pages 19-21
Abstract Interpretation with Applications to Timing Validation....Pages 22-36
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis....Pages 37-51
Monitoring Atomicity in Concurrent Programs....Pages 52-65
Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings....Pages 66-79
A Hybrid Type System for Lock-Freedom of Mobile Processes....Pages 80-93
Implied Set Closure and Its Application to Memory Consistency Verification....Pages 94-106
Effective Program Verification for Relaxed Memory Models....Pages 107-120
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses....Pages 121-134
Automated Assume-Guarantee Reasoning by Abstraction Refinement....Pages 135-148
Local Proofs for Linear-Time Properties of Concurrent Programs....Pages 149-161
Probabilistic CEGAR....Pages 162-175
Computing Differential Invariants of Hybrid Systems as Fixedpoints....Pages 176-189
Constraint-Based Approach for Analysis of Hybrid Systems....Pages 190-203
AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems....Pages 204-208
FS hell : Systematic Test Case Generation for Dynamic Analysis and Measurement....Pages 209-213
Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems....Pages 214-226
Conflict-Tolerant Features....Pages 227-239
Ranking Automata and Games for Prioritized Requirements....Pages 240-253
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations....Pages 254-267
Linear Arithmetic with Stars....Pages 268-280
Inferring Congruence Equations Using SAT....Pages 281-293
The Barcelogic SMT Solver....Pages 294-298
The MathSAT 4 SMT Solver....Pages 299-303
CSIsat : Interpolation for LA+EUF....Pages 304-308
Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B....Pages 309-313
Heap Assumptions on Demand....Pages 314-327
Proving Conditional Termination....Pages 328-340
Monotonic Abstraction for Programs with Dynamic Memory Heaps....Pages 341-354
Enhancing Program Verification with Lemmas....Pages 355-369
A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis....Pages 370-384
Scalable Shape Analysis for Systems Code....Pages 385-398
Thread Quantification for Concurrent Shape Analysis....Pages 399-413
The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols....Pages 414-418
The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis....Pages 419-422
Jakstab: A Static Analysis Platform for Binaries....Pages 423-427
THOR: A Tool for Reasoning about Shape and Arithmetic....Pages 428-432
Functional Verification of Power Gated Designs by Compositional Reasoning....Pages 433-445
A Practical Approach to Word Level Model Checking of Industrial Netlists....Pages 446-458
Validating High-Level Synthesis....Pages 459-472
An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths....Pages 473-486
Application of Formal Word-Level Analysis to Constrained Random Simulation....Pages 487-490
Producing Short Counterexamples Using “Crucial Events”....Pages 491-503
Discriminative Model Checking....Pages 504-516
Correcting a Space-Efficient Simulation Algorithm....Pages 517-529
Semi-external LTL Model Checking....Pages 530-542
QMC : A Model Checker for Quantum Systems....Pages 543-547
T(O)RMC: A Tool for ( ω )-Regular Model Checking....Pages 548-551
Faster Than Uppaal ?....Pages 552-555
Back Matter....Pages -
