LEADER 06741nam 22007575 450 001 996465780103316 005 20220712163616.0 010 $a3-540-44585-4 024 7 $a10.1007/3-540-44585-4 035 $a(CKB)1000000000211511 035 $a(SSID)ssj0000322074 035 $a(PQKBManifestationID)11257612 035 $a(PQKBTitleCode)TC0000322074 035 $a(PQKBWorkID)10281190 035 $a(PQKB)10626655 035 $a(DE-He213)978-3-540-44585-2 035 $a(MiAaPQ)EBC3073005 035 $a(PPN)15519982X 035 $a(EXLCZ)991000000000211511 100 $a20121227d2001 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aComputer Aided Verification$b[electronic resource] $e13th International Conference, CAV 2001, Paris, France, July 18-22, 2001. Proceedings /$fedited by Gerard Berry, Hubert Comon, Alain Finkel 205 $a1st ed. 2001. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2001. 215 $a1 online resource (XIII, 522 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v2102 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-42345-1 320 $aIncludes bibliographical references at the end of each chapters and index. 327 $aInvited Talk -- Software Documentation and the Verification Process -- Model Checking and Theorem Proving -- Certifying Model Checkers -- Formalizing a JVML Verifier for Initialization in a Theorem Prover -- Automated Inductive Verification of Parameterized Protocols? -- Automata Techniques -- Efficient Model Checking Via Büchi Tableau Automata? -- Fast LTL to Büchi Automata Translation -- A Practical Approach to Coverage in Model Checking -- Verification Core Technology -- A Fast Bisimulation Algorithm -- Symmetry and Reduced Symmetry in Model Checking? -- Transformation-Based Verification Using Generalized Retiming -- BDD and Decision Procedures -- Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions -- CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination -- Finite Instantiations in Equivalence Logic with Uninterpreted Functions -- Abstraction and Refinement -- Model Checking with Formula-Dependent Abstract Models -- Verifying Network Protocol Implementations by Symbolic Refinement Checking -- Automatic Abstraction for Verification of Timed Circuits and Systems? -- Combinations -- Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM? -- Analysis of Recursive State Machines -- Parameterized Verification with Automatically Computed Inductive Assertions? -- Tool Presentations: Rewriting and Theorem-Proving Techniques -- EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations -- AGVI ? Automatic Generation, Verification, and Implementation of Security Protocols -- ICS: Integrated Canonizer and Solver? -- µCRL: A Toolset for Analysing Algebraic Specifications -- Truth/SLC ? A Parallel Verification Platform for Concurrent Systems -- The SLAM Toolkit -- Invited Talk -- Java Bytecode Verification: An Overview -- Infinite State Systems -- Iterating Transducers -- Attacking Symbolic State Explosion -- A Unifying Model Checking Approach for Safety Properties of Parameterized Systems -- A BDD-Based Model Checker for Recursive Programs -- Temporal Logics and Verification -- Model Checking the World Wide Web? -- Distributed Symbolic Model Checking for ?-Calculus -- Tool Presentations: Model-Checking and Automata Techniques -- The Temporal Logic Sugar -- TReX: A Tool for Reachability Analysis of Complex Systems -- BOOSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstraction -- SDLcheck: A Model Checking Tool -- EASN: Integrating ASN.1 and Model Checking -- Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams -- TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems? -- Microprocessor Verification, Cache Coherence -- Microarchitecture Verification by Compositional Model Checking -- Rewriting for Symbolic Execution of State Machine Models -- Using Timestamping and History Variables to Verify Sequential Consistency -- SAT, BDDs, and Applications -- Benefits of Bounded Model Checking at an Industrial Setting -- Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers -- Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m) -- Timed Automata -- Job-Shop Scheduling Using Timed Automata? -- As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata -- Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks. 606 $aDatabase management 606 $aComputers 606 $aSoftware engineering 606 $aComputer logic 606 $aMathematical logic 606 $aArtificial intelligence 606 $aDatabase Management$3https://scigraph.springernature.com/ontologies/product-market-codes/I18024 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 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$aDatabase management. 615 0$aComputers. 615 0$aSoftware engineering. 615 0$aComputer logic. 615 0$aMathematical logic. 615 0$aArtificial intelligence. 615 14$aDatabase Management. 615 24$aTheory of Computation. 615 24$aSoftware Engineering/Programming and Operating Systems. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 676 $a005.74 702 $aBerry$b Gerard$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aComon$b Hubert$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aFinkel$b Alain$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a996465780103316 996 $aComputer Aided Verification$93027789 997 $aUNISA