Limit search to available items
Book Cover
Author CAV (Conference) (18th : 2006 : Seattle, Wash.)

Title Computer aided verification : 18th international conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006 : proceedings / Thomas Ball, Robert B. Jones (eds.)
Published Berlin ; New York : Springer, ©2006


Description 1 online resource (xv, 564 pages) : illustrations
Series Lecture notes in computer science, 0302-9743 ; 4144
LNCS sublibrary. SL 1, Theoretical computer science and general issues
Lecture notes in computer science ; 4144.
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
Contents Invited Talks -- Formal Specifications on Industrial-Strength Code--From Myth to Reality -- I Think I Voted: E-Voting vs. Democracy -- Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs -- The Ideal of Verified Software -- Session 1. Automata -- Antichains: A New Algorithm for Checking Universality of Finite Automata -- Safraless Compositional Synthesis -- Minimizing Generalized Büchi Automata -- Session 2. Tools Papers -- Ticc: A Tool for Interface Compatibility and Composition -- FAST Extended Release -- Session 3. Arithmetic -- Don't Care Words with an Application to the Automata-Based Approach for Real Addition -- A Fast Linear-Arithmetic Solver for DPLL(T) -- Session 4. SAT and Bounded Model Checking -- Bounded Model Checking for Weak Alternating Büchi Automata -- Deriving Small Unsatisfiable Cores with Dominators -- Session 5. Abstraction/Refinement -- Lazy Abstraction with Interpolants -- Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop -- Counterexamples with Loops for Predicate Abstraction -- Session 6. Tools Papers -- cascade: C Assertion Checker and Deductive Engine -- Yasm: A Software Model-Checker for Verification and Refutation -- Session 7. Symbolic Trajectory Evaluation -- SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation -- Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation -- Session 8. Property Specification and Verification -- Some Complexity Results for SystemVerilog Assertions -- Check It Out: On the Efficient Formal Verification of Live Sequence Charts -- Session 9. Time -- Symmetry Reduction for Probabilistic Model Checking -- Communicating Timed Automata: The More Synchronous, the More Difficult to Verify -- Allen Linear (Interval) Temporal Logic -- Translation to LTL and Monitor Synthesis -- Session 10. Tools Papers -- DiVinE -- A Tool for Distributed Verification -- EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation -- Session 11. Concurrency -- Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions -- Model Checking Multithreaded Programs with Asynchronous Atomic Methods -- Causal Atomicity -- Session 12. Trees, Pushdown Systems and Boolean Programs -- Languages of Nested Trees -- Improving Pushdown System Model Checking -- Repair of Boolean Programs with an Application to C -- Session 13. Termination -- Termination of Integer Linear Programs -- Automatic Termination Proofs for Programs with Shape-Shifting Heaps -- Termination Analysis with Calling Context Graphs -- Session 14. Tools Papers -- Terminator: Beyond Safety -- CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools -- Session 15. Abstract Interpretation -- SMT Techniques for Fast Predicate Abstraction -- The Power of Hybrid Acceleration -- Lookahead Widening -- Session 16. Tools Papers -- The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover -- LEVER: A Tool for Learning Based Verification -- Session 17. Memory Consistency -- Formal Verification of a Lazy Concurrent List-Based Set Algorithm -- Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study -- Fast and Generalized Polynomial Time Memory Consistency Verification -- Session 18. Shape Analysis -- Programs with Lists Are Counter Automata -- Lazy Shape Analysis -- Abstraction for Shape Analysis with Fast and Precise Transformers
Analysis ontwerp
computer sciences
kunstmatige intelligentie
artificial intelligence
software engineering
Information and Communication Technology (General)
Informatie- en communicatietechnologie (algemeen)
Bibliography Includes bibliographical references and index
Notes English
Print version record
Subject Computer software -- Verification -- Congresses
Integrated circuits -- Verification -- Congresses
Integrated circuits -- Verification.
Circuits intégrés -- Vérification.
Logiciels -- Vérification.
Computer software -- Verification.
Computer software -- Verification.
Integrated circuits -- Verification.
Genre/Form Conference papers and proceedings.
Conference papers and proceedings.
Actes de congrès.
Form Electronic book
Author Ball, Thomas, 1965-
Jones, Robert B. (Robert Brent), 1969-
ISBN 9783540374114
Other Titles CAV 2006