000 04922nam a22006135i 4500
001 978-3-540-45069-6
003 DE-He213
005 20240423132526.0
007 cr nn 008mamaa
008 121227s2003 gw | s |||| 0|eng d
020 _a9783540450696
_9978-3-540-45069-6
024 7 _a10.1007/b11831
_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] :
_b15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings /
_cedited by Warren A. Hunt, Jr., Fabio Somenzi.
250 _a1st ed. 2003.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2003.
300 _aXII, 462 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v2725
505 0 _aExtending Bounded Model Checking -- Interpolation and SAT-Based Model Checking -- Bounded Model Checking and Induction: From Refutation to Verification -- Symbolic Model Checking -- Reasoning with Temporal Logic on Truncated Paths -- Structural Symbolic CTL Model Checking of Asynchronous Systems -- A Work-Efficient Distributed Algorithm for Reachability Analysis -- Games, Trees, and Counters -- Modular Strategies for Infinite Games on Recursive Graphs -- Fast Mu-Calculus Model Checking when Tree-Width Is Bounded -- Dense Counter Machines and Verification Problems -- Tool Presentations I -- TRIM: A Tool for Triggered Message Sequence Charts -- Model Checking Multi-Agent Programs with CASP -- Monitoring Temporal Rules Combined with Time Series -- FAST: Fast Acceleration of Symbolic Transition Systems -- Rabbit: A Tool for BDD-Based Verification of Real-Time Systems -- Abstraction I -- Making Predicate Abstraction Efficient: -- A Symbolic Approach to Predicate Abstraction -- Unbounded, Fully Symbolic Model Checking of Timed Automata Using Boolean Methods -- Dense Time -- Digitizing Interval Duration Logic -- Timed Control with Partial Observability -- Hybrid Acceleration Using Real Vector Automata -- Tool Presentations II -- Abstraction and BDDs Complement SAT-Based BMC in DiVer -- TLQSolver: A Temporal Logic Query Checker -- Evidence Explorer: A Tool for Exploring Model-Checking Proofs -- HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols -- Infinite State Systems -- Iterating Transducers in the Large -- Algorithmic Improvements in Regular Model Checking -- Efficient Image Computation in Infinite State Model Checking -- Abstraction II -- Thread-Modular Abstraction Refinement -- A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement -- Abstraction for Branching Time Properties -- Applications -- Certifying Optimality of State Estimation Programs -- Domain-Specific Optimization in Automata Learning -- Model Checking Conformance with Scenario-Based Specifications -- Theorem Proving -- Deductive Verification of Advanced Out-of-Order Microprocessors -- Theorem Proving Using Lazy Proof Explication -- Automata-Based Verification -- Enhanced Vacuity Detection in Linear Temporal Logic -- Bridging the Gap between Fair Simulation and Trace Inclusion -- An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic -- Invariants -- Strengthening Invariants by Symbolic Consistency Testing -- Linear Invariant Generation Using Non-linear Constraint Solving -- Explicit Model Checking -- To Store or Not to Store -- Calculating ?-Confluence Compositionally.
650 0 _aComputer science.
650 0 _aLogic design.
650 0 _aComputers, Special purpose.
650 0 _aSoftware engineering.
650 0 _aMachine theory.
650 1 4 _aTheory of Computation.
650 2 4 _aComputer Science Logic and Foundations of Programming.
650 2 4 _aLogic Design.
650 2 4 _aSpecial Purpose and Application-Based Systems.
650 2 4 _aSoftware Engineering.
650 2 4 _aFormal Languages and Automata Theory.
700 1 _aHunt, Jr., Warren A.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aSomenzi, Fabio.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540405245
776 0 8 _iPrinted edition:
_z9783662186855
830 0 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v2725
856 4 0 _uhttps://doi.org/10.1007/b11831
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
912 _aZDB-2-BAE
942 _cSPRINGER
999 _c188711
_d188711