Computer Aided Verification: 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings (Lecture Notes in Computer Science (5123))

Annotation 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 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 - This book constitutes the proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014.