LEADER 05909nam 22007935 450 001 9910767527303321 005 20200629203507.0 010 $a3-540-27813-3 024 7 $a10.1007/b98490 035 $a(CKB)1000000000212451 035 $a(SSID)ssj0000127767 035 $a(PQKBManifestationID)11141130 035 $a(PQKBTitleCode)TC0000127767 035 $a(PQKBWorkID)10062561 035 $a(PQKB)10961635 035 $a(DE-He213)978-3-540-27813-9 035 $a(MiAaPQ)EBC3088566 035 $a(PPN)155165216 035 $a(EXLCZ)991000000000212451 100 $a20121227d2004 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aComputer Aided Verification $e16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings /$fedited by Rajeev Alur, Doron A. Peled 205 $a1st ed. 2004. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2004. 215 $a1 online resource (XII, 536 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v3114 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-22342-8 320 $aIncludes bibliographical references at the end of each chapters and index. 327 $aRob Tristan Gerth: 1956?2003 -- Static Program Analysis via 3-Valued Logic -- Deductive Verification of Pipelined Machines Using First-Order Quantification -- A Formal Reduction for Lock-Free Parallel Algorithms -- An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking -- Termination of Linear Programs -- Symbolic Model Checking of Non-regular Properties -- Proving More Properties with Bounded Model Checking -- Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings -- Using Interface Refinement to Integrate Formal Verification into the Design Cycle -- Indexed Predicate Discovery for Unbounded System Verification -- Range Allocation for Separation Logic -- An Experimental Evaluation of Ground Decision Procedures -- DPLL(T): Fast Decision Procedures -- Verifying ?-Regular Properties of Markov Chains -- Statistical Model Checking of Black-Box Probabilistic Systems -- Compositional Specification and Model Checking in GSTE -- GSTE Is Partitioned Model Checking -- Stuck-Free Conformance -- Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors -- Functional Dependency for Verification Reduction -- Verification via Structure Simulation -- Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures -- Abstraction-Based Satisfiability Solving of Presburger Arithmetic -- Widening Arithmetic Automata -- Why Model Checking Can Improve WCET Analysis -- Regular Model Checking for LTL(MSO) -- Image Computation in Infinite State Model Checking -- Abstract Regular Model Checking -- Global Model-Checking of Infinite-State Systems -- QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings -- Verification of an Advanced mips-Type Out-of-Order Execution Algorithm -- Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values -- Efficient Modeling of Embedded Memories in Bounded Model Checking -- Understanding Counterexamples with explain -- Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement -- JNuke: Efficient Dynamic Analysis for Java -- The HiVy Tool Set -- ObsSlice: A Timed Automata Slicer Based on Observers -- The UCLID Decision Procedure -- MCK: Model Checking the Logic of Knowledge -- Zing: A Model Checker for Concurrent Software -- The Mec 5 Model-Checker -- PlayGame: A Platform for Diagnostic Games -- SAL 2 -- Formal Analysis of Java Programs in JavaFAN -- A Toolset for Modelling and Verification of GALS Systems -- WSAT: A Tool for Formal Analysis of Web Services -- CVC Lite: A New Implementation of the Cooperating Validity Checker -- CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking -- Mechanical Mathematical Methods for Microprocessor Verification. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v3114 606 $aComputers 606 $aSoftware engineering 606 $aLogic design 606 $aComputer logic 606 $aMathematical logic 606 $aArtificial intelligence 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aLogic Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I12050 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 615 0$aComputers. 615 0$aSoftware engineering. 615 0$aLogic design. 615 0$aComputer logic. 615 0$aMathematical logic. 615 0$aArtificial intelligence. 615 14$aTheory of Computation. 615 24$aSoftware Engineering. 615 24$aLogic Design. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 676 $a005.1 702 $aAlur$b Rajeev$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aPeled$b Doron A$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910767527303321 996 $aComputer Aided Verification$93027789 997 $aUNINA