Computer Aided Verification: 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings

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 -