LEADER 05848nam 22007935 450 001 996465898403316 005 20200630015523.0 010 $a3-540-45069-6 024 7 $a10.1007/b11831 035 $a(CKB)1000000000212077 035 $a(SSID)ssj0000322075 035 $a(PQKBManifestationID)11282750 035 $a(PQKBTitleCode)TC0000322075 035 $a(PQKBWorkID)10283245 035 $a(PQKB)10014654 035 $a(DE-He213)978-3-540-45069-6 035 $a(MiAaPQ)EBC3088048 035 $a(PPN)155166050 035 $a(EXLCZ)991000000000212077 100 $a20121227d2003 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aComputer Aided Verification$b[electronic resource] $e15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings /$fedited by Warren A. Hunt, Jr., Fabio Somenzi 205 $a1st ed. 2003. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2003. 215 $a1 online resource (XII, 462 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v2725 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-40524-0 320 $aIncludes bibliographical references at the end of each chapters and index. 327 $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. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v2725 606 $aComputers 606 $aComputer logic 606 $aLogic design 606 $aSpecial purpose computers 606 $aSoftware engineering 606 $aMathematical logic 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aLogic Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I12050 606 $aSpecial Purpose and Application-Based Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I13030 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 615 0$aComputers. 615 0$aComputer logic. 615 0$aLogic design. 615 0$aSpecial purpose computers. 615 0$aSoftware engineering. 615 0$aMathematical logic. 615 14$aTheory of Computation. 615 24$aLogics and Meanings of Programs. 615 24$aLogic Design. 615 24$aSpecial Purpose and Application-Based Systems. 615 24$aSoftware Engineering. 615 24$aMathematical Logic and Formal Languages. 676 $a005.14 702 $aHunt$b Jr., Warren A$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSomenzi$b Fabio$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465898403316 996 $aComputer Aided Verification$9772228 997 $aUNISA