Computer Aided Verification : 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings / edited by Thomas Ball, Robert B. Jones
(Theoretical Computer Science and General Issues. ISSN:25122029 ; 4144)
データ種別 | 電子ブック |
---|---|
版 | 1st ed. 2006. |
出版者 | (Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer) |
出版年 | 2006 |
大きさ | XV, 564 p : online resource |
著者標目 | Ball, Thomas editor Jones, Robert B editor SpringerLink (Online service) |
書誌詳細を非表示
一般注記 | 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 HTTP:URL=https://doi.org/10.1007/11817963 |
---|---|
件 名 | LCSH:Computer science LCSH:Software engineering LCSH:Machine theory LCSH:Artificial intelligence LCSH:Logic design FREE:Theory of Computation FREE:Computer Science Logic and Foundations of Programming FREE:Software Engineering FREE:Formal Languages and Automata Theory FREE:Artificial Intelligence FREE:Logic Design |
分 類 | LCC:QA75.5-76.95 DC23:004.0151 |
書誌ID | EB00003432 |
ISBN | 9783540374114 |
類似資料
この資料の利用統計
このページへのアクセス回数:12回
※2019年3月27日以降
全貸出数:0回
(1年以内の貸出:0回)
※2019年3月27日以降