LEADER 06184nam 22007455 450 001 996465602503316 005 20230406051307.0 010 $a3-540-37411-6 024 7 $a10.1007/11817963 035 $a(CKB)1000000000233072 035 $a(SSID)ssj0000316851 035 $a(PQKBManifestationID)11246854 035 $a(PQKBTitleCode)TC0000316851 035 $a(PQKBWorkID)10276292 035 $a(PQKB)10292723 035 $a(DE-He213)978-3-540-37411-4 035 $a(MiAaPQ)EBC3068225 035 $a(PPN)123137381 035 $a(EXLCZ)991000000000233072 100 $a20101221d2006 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aComputer Aided Verification$b[electronic resource] $e18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings /$fedited by Thomas Ball, Robert B. Jones 205 $a1st ed. 2006. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2006. 215 $a1 online resource (XV, 564 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4144 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-37406-X 320 $aIncludes bibliographical references and index. 327 $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. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4144 606 $aComputer science 606 $aSoftware engineering 606 $aMachine theory 606 $aArtificial intelligence 606 $aLogic design 606 $aTheory of Computation 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aFormal Languages and Automata Theory 606 $aArtificial Intelligence 606 $aLogic Design 615 0$aComputer science. 615 0$aSoftware engineering. 615 0$aMachine theory. 615 0$aArtificial intelligence. 615 0$aLogic design. 615 14$aTheory of Computation. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aFormal Languages and Automata Theory. 615 24$aArtificial Intelligence. 615 24$aLogic Design. 676 $a004.24 702 $aBall$b Thomas$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aJones$b Robert B$g(Robert Brent),$f1969-.$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aCAV (Conference) 906 $aBOOK 912 $a996465602503316 996 $aComputer Aided Verification$9772228 997 $aUNISA