Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 18-22, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.)

Resource Information

The instance Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 18-22, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.) represents a material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries. This resource is a combination of several types including: Instance, Electronic.

Image

http://images.btol.com/ContentCafe/Jacket.aspx?UserID=ebsco-test&Password=ebsco-test&Return=T&Value=9783540445852&Type=L

Label

Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 18-22, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.)

Title remainder

13th International conference, CAV 2001, Paris, France, July 18-22, 2001 : proceedings

Statement of responsibility

Gérard Berry, Hubert Comon, Alain Finkel (eds.)

Instantiates

• Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 18-22, 2001 : proceedings

Publication

• Berlin, Springer, 2001

Bibliography note

Includes bibliographical references and index

Carrier category

online resource

Carrier category code

• cr

Carrier MARC source

rdacarrier

Content category

text

Content type code

• txt

Content type MARC source

rdacontent

Contents

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

Control code

213933854

Dimensions

unknown

Extent

1 online resource (xiii, 520 pages).

Form of item

online

Isbn

9783540445852

Media category

computer

Media MARC source

rdamedia

Media type code

• c

Other control number

• 10.1007/3-540-44585-4
• 9783540423454

http://library.link/vocab/ext/overdrive/overdriveId

3540423451

Record ID

.b130094213

Sound

unknown sound

Specific material designation

remote

System control number

(OCoLC)213933854