Computer Aided Verification 计算机辅助验证

书籍目录

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 SoftwareSession 1. Automata  Antichains: A New Algorithm for Checking Universality of Finite Automata  Safraless Compositional Synthesis.  Minimizing Generalized Biichi AutomataSession 2. Tools Papers  Ticc: A Tool for Interface Compatibility and Composition  FAST Extended ReleaseSession 3. Arithmetic  Don't Care Words with an Application to the Automata-Base 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 Biichi Automal  Deriving Small Unsatisfiable Cores with DominatorsSession 5. Abstraction/Refinement  Lazy Abstraction with Interpolants  Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop Counterexamples with Loops for Predicate AbstractionSession 6. Tools Papers  Cascade: C Assertion Checker and Deductive Engine  YASM: A Software Model-Checker for Verification and Refutati,Session 7. Symbolic Trajectory Evaluation  SAT-Based Assistance in Abstraction Refinement for Symboli, Trajectory Evaluation  Automatic Refinement and Vacuity Detection for Symbolic Trajectory EvaluationSession 8. Property Specification and Verification Session 9. Time Session 10. Tools Papers Session 11. ConcurrencySession 12. Trees,Pushdown Systems and Boolean ProgramsSession 13. Termination Session 14. Tools Papers Session 15. Abstract Interpretation Session 16. Tools Papers Session 17. Memory Consistency Session 18. Shape Analysis Author Index

作者简介

　　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.

 Computer Aided Verification 计算机辅助验证下载