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

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

Label
Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 18-22, 2001 : proceedings
Title
Computer aided verification
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.)
Title variation
CAV 2001
Creator
Contributor
Subject
Genre
Language
eng
Summary
This book constitutes the refereed proceedings of the 13th International Conference on Computer Aided Verification, CAV 2001, held in Paris, France in July 2001. The 33 revised full papers presented were carefully reviewed and selected from 106 regular paper submissions; also included are 13 reviewed tool presentations selected from 27 submissions. The book offers topical sections on model checking and theorem proving, automata techniques, verification core technology, BDD and decision trees, abstraction and refinement, combinations, infinite state systems, temporal logics and verification, microprocessor verification and cache coherence, SAT and applications, and timed automata
Member of
Cataloging source
CUT
Dewey number
004.24
Index
index present
LC call number
QA76.76.V47
LC item number
C38 2001eb
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2001
http://bibfra.me/vocab/lite/meetingName
CAV (Conference)
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorDate
  • 1948-
  • 1958-
http://library.link/vocab/relatedWorkOrContributorName
  • Comon, Hubert
  • Berry, Gérard
  • Finkel, A.
  • LINK (Online service)
Series statement
  • Lecture notes in computer science,
  • Lecture notes in computer science. Lecture notes in artificial intelligence
Series volume
2102
http://library.link/vocab/subjectName
  • Computer software
  • Integrated circuits
  • Computer software
  • Integrated circuits
Label
Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 18-22, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.), (electronic resource)
Link
http://dx.doi.org/10.1007/3-540-44585-4
Instantiates
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online bron
Carrier category code
  • cr
Carrier MARC source
rdacarrier/dut
Content category
tekst
Content type code
  • txt
Content type MARC source
rdacontent/dut
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
Dimensions
unknown
Extent
1 online resource (xiii, 520 p.)
Form of item
online
Isbn
9783540445852
Isbn Type
(electronic bk.)
Media category
computer
Media MARC source
rdamedia/dut
Media type code
  • c
Sound
unknown sound
Specific material designation
remote
System control number
  • (OCoLC)213933854
  • (OCoLC)ocn213933854
Label
Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 18-22, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.), (electronic resource)
Link
http://dx.doi.org/10.1007/3-540-44585-4
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online bron
Carrier category code
  • cr
Carrier MARC source
rdacarrier/dut
Content category
tekst
Content type code
  • txt
Content type MARC source
rdacontent/dut
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
Dimensions
unknown
Extent
1 online resource (xiii, 520 p.)
Form of item
online
Isbn
9783540445852
Isbn Type
(electronic bk.)
Media category
computer
Media MARC source
rdamedia/dut
Media type code
  • c
Sound
unknown sound
Specific material designation
remote
System control number
  • (OCoLC)213933854
  • (OCoLC)ocn213933854

Library Locations

  • Architecture LibraryBorrow it
    Gould Hall 830 Van Vleet Oval Rm. 105, Norman, OK, 73019, US
    35.205706 -97.445050
  • Bizzell Memorial LibraryBorrow it
    401 W. Brooks St., Norman, OK, 73019, US
    35.207487 -97.447906
  • Boorstin CollectionBorrow it
    401 W. Brooks St., Norman, OK, 73019, US
    35.207487 -97.447906
  • Chinese Literature Translation ArchiveBorrow it
    401 W. Brooks St., RM 414, Norman, OK, 73019, US
    35.207487 -97.447906
  • Engineering LibraryBorrow it
    Felgar Hall 865 Asp Avenue, Rm. 222, Norman, OK, 73019, US
    35.205706 -97.445050
  • Fine Arts LibraryBorrow it
    Catlett Music Center 500 West Boyd Street, Rm. 20, Norman, OK, 73019, US
    35.210371 -97.448244
  • Harry W. Bass Business History CollectionBorrow it
    401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • History of Science CollectionsBorrow it
    401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • John and Mary Nichols Rare Books and Special CollectionsBorrow it
    401 W. Brooks St., Rm. 509NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • Library Service CenterBorrow it
    2601 Technology Place, Norman, OK, 73019, US
    35.185561 -97.398361
  • Price College Digital LibraryBorrow it
    Adams Hall 102 307 West Brooks St., Norman, OK, 73019, US
    35.210371 -97.448244
  • Western History CollectionsBorrow it
    Monnet Hall 630 Parrington Oval, Rm. 300, Norman, OK, 73019, US
    35.209584 -97.445414
Processing Feedback ...