This book constitutes the refereed proceedings of the 18th International Conference on Computer Aided Verification, CAV 2006, held in Seattle, WA, USA in August 2006 as part of the 4th Federated Logic Conference, FLoC 2006.
The 35 revised full papers presented together with 10 tool papers and 4 invited papers were carefully reviewed and selected from 144 submissions adressing all current issues in computer aided verification and model checking - from foundational and methodological issues ranging to the evaluation of major tools and systems. The papers are organized in topical sections on automata, arithmetic, SAT and bounded model checking, abstraction/refinement, symbolic trajectory evaluation, property specification and verification, time, concurrency, trees, pushdown systems and boolean programs, termination, abstract interpretation, memory consistency, and shape analysis.
Author(s): Manuvir Das (auth.), Thomas Ball, Robert B. Jones (eds.)
Series: Lecture Notes in Computer Science 4144 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2006
Language: English
Pages: 564
Tags: Logics and Meanings of Programs; Software Engineering; Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Logic Design
Front Matter....Pages -
Formal Specifications on Industrial-Strength Code—From Myth to Reality....Pages 1-1
I Think I Voted: E-Voting vs. Democracy....Pages 2-2
Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs....Pages 3-4
The Ideal of Verified Software....Pages 5-16
Antichains: A New Algorithm for Checking Universality of Finite Automata....Pages 17-30
Safraless Compositional Synthesis....Pages 31-44
Minimizing Generalized Büchi Automata....Pages 45-58
Ticc : A Tool for Interface Compatibility and Composition....Pages 59-62
FAST Extended Release....Pages 63-66
Don’t Care Words with an Application to the Automata-Based Approach for Real Addition....Pages 67-80
A Fast Linear-Arithmetic Solver for DPLL(T)....Pages 81-94
Bounded Model Checking for Weak Alternating Büchi Automata....Pages 95-108
Deriving Small Unsatisfiable Cores with Dominators....Pages 109-122
Lazy Abstraction with Interpolants....Pages 123-136
Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop....Pages 137-151
Counterexamples with Loops for Predicate Abstraction....Pages 152-165
cascade: C Assertion Checker and Deductive Engine....Pages 166-169
Yasm : A Software Model-Checker for Verification and Refutation....Pages 170-174
SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation....Pages 175-189
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation....Pages 190-204
Some Complexity Results for SystemVerilog Assertions....Pages 205-218
Check It Out: On the Efficient Formal Verification of Live Sequence Charts....Pages 219-233
Symmetry Reduction for Probabilistic Model Checking....Pages 234-248
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify....Pages 249-262
Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis....Pages 263-277
DiVinE – A Tool for Distributed Verification....Pages 278-281
EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation....Pages 282-285
Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions....Pages 286-299
Model Checking Multithreaded Programs with Asynchronous Atomic Methods....Pages 300-314
Causal Atomicity....Pages 315-328
Languages of Nested Trees....Pages 329-342
Improving Pushdown System Model Checking....Pages 343-357
Repair of Boolean Programs with an Application to C....Pages 358-371
Termination of Integer Linear Programs....Pages 372-385
Automatic Termination Proofs for Programs with Shape-Shifting Heaps....Pages 386-400
Termination Analysis with Calling Context Graphs....Pages 401-414
Terminator : Beyond Safety....Pages 415-418
CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools....Pages 419-423
SMT Techniques for Fast Predicate Abstraction....Pages 424-437
The Power of Hybrid Acceleration....Pages 438-451
Lookahead Widening....Pages 452-466
The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover....Pages 467-470
LEVER: A Tool for Learning Based Verification....Pages 471-474
Formal Verification of a Lazy Concurrent List-Based Set Algorithm....Pages 475-488
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study....Pages 489-502
Fast and Generalized Polynomial Time Memory Consistency Verification....Pages 503-516
Programs with Lists Are Counter Automata....Pages 517-531
Lazy Shape Analysis....Pages 532-546
Abstraction for Shape Analysis with Fast and Precise Transformers....Pages 547-561
Back Matter....Pages -
