Computer Aided Verification 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings /
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2006.
|
| Σειρά: | Lecture Notes in Computer Science,
4144 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- 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.
