06716nam 22007575 450 991014359450332120220712163616.03-540-44585-410.1007/3-540-44585-4(CKB)1000000000211511(SSID)ssj0000322074(PQKBManifestationID)11257612(PQKBTitleCode)TC0000322074(PQKBWorkID)10281190(PQKB)10626655(DE-He213)978-3-540-44585-2(MiAaPQ)EBC3073005(PPN)15519982X(EXLCZ)99100000000021151120121227d2001 u| 0engurnn#008mamaatxtccrComputer Aided Verification 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001. Proceedings /edited by Gerard Berry, Hubert Comon, Alain Finkel1st ed. 2001.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2001.1 online resource (XIII, 522 p.)Lecture Notes in Computer Science,0302-9743 ;2102Bibliographic Level Mode of Issuance: Monograph3-540-42345-1 Includes bibliographical references at the end of each chapters and index.Invited 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.Database managementComputersSoftware engineeringComputer logicMathematical logicArtificial intelligenceDatabase Managementhttps://scigraph.springernature.com/ontologies/product-market-codes/I18024Theory of Computationhttps://scigraph.springernature.com/ontologies/product-market-codes/I16005Software Engineering/Programming and Operating Systemshttps://scigraph.springernature.com/ontologies/product-market-codes/I14002Logics and Meanings of Programshttps://scigraph.springernature.com/ontologies/product-market-codes/I1603XMathematical Logic and Formal Languageshttps://scigraph.springernature.com/ontologies/product-market-codes/I16048Artificial Intelligencehttps://scigraph.springernature.com/ontologies/product-market-codes/I21000Database management.Computers.Software engineering.Computer logic.Mathematical logic.Artificial intelligence.Database Management.Theory of Computation.Software Engineering/Programming and Operating Systems.Logics and Meanings of Programs.Mathematical Logic and Formal Languages.Artificial Intelligence.005.74Berry Gerardedthttp://id.loc.gov/vocabulary/relators/edtComon Hubertedthttp://id.loc.gov/vocabulary/relators/edtFinkel Alainedthttp://id.loc.gov/vocabulary/relators/edtBOOK9910143594503321Computer Aided Verification3027789UNINA