Computer Aided Verification 计算机辅助验证

2006-9  

1 (2006年9月25日)  

Thomas Ball  

564  

　　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.

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

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