000 05862nam a22006015i 4500
001 978-3-540-37411-4
003 DE-He213
005 20240730194215.0
007 cr nn 008mamaa
008 101221s2006 gw | s |||| 0|eng d
020 _a9783540374114
_9978-3-540-37411-4
024 7 _a10.1007/11817963
_2doi
050 4 _aQA75.5-76.95
072 7 _aUYA
_2bicssc
072 7 _aCOM014000
_2bisacsh
072 7 _aUYA
_2thema
082 0 4 _a004.0151
_223
245 1 0 _aComputer Aided Verification
_h[electronic resource] :
_b18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings /
_cedited by Thomas Ball, Robert B. Jones.
250 _a1st ed. 2006.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2006.
300 _aXV, 564 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v4144
505 0 _aInvited 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.
650 0 _aComputer science.
_99832
650 0 _aSoftware engineering.
_94138
650 0 _aMachine theory.
_9156144
650 0 _aArtificial intelligence.
_93407
650 0 _aLogic design.
_93686
650 1 4 _aTheory of Computation.
_9156145
650 2 4 _aComputer Science Logic and Foundations of Programming.
_942203
650 2 4 _aSoftware Engineering.
_94138
650 2 4 _aFormal Languages and Automata Theory.
_9156146
650 2 4 _aArtificial Intelligence.
_93407
650 2 4 _aLogic Design.
_93686
700 1 _aBall, Thomas.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9156147
700 1 _aJones, Robert B.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9156148
710 2 _aSpringerLink (Online service)
_9156149
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540374060
776 0 8 _iPrinted edition:
_z9783540827825
830 0 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v4144
_9156150
856 4 0 _uhttps://doi.org/10.1007/11817963
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c95081
_d95081