The Resource Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 1822, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.)
Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 1822, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.)
Resource Information
The item Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 1822, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries.This item is available to borrow from 1 library branch.
Resource Information
The item Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 1822, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries.
This item is available to borrow from 1 library branch.
 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
 Language
 eng
 Extent
 1 online resource (xiii, 520 pages).
 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?
 TransformationBased Verification Using Generalized Retiming
 BDD and Decision Procedures
 MetaBDDs: 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 FormulaDependent 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 TheoremProving 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 BDDBased Model Checker for Recursive Programs
 Temporal Logics and Verification
 Model Checking the World Wide Web?
 Distributed Symbolic Model Checking for?Calculus
 Tool Presentations: ModelChecking 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 WordLevel Abstraction
 SDLcheck: A Model Checking Tool
 EASN: Integrating ASN. 1 and Model Checking
 Rtdt: A FrontEnd for Efficient Model Checking of Synchronous Timing Diagrams
 TAXYS: A Tool for the Development and Verification of RealTime 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
 JobShop Scheduling Using Timed Automata?
 As Cheap as Possible: Effcient CostOptimal Reachability for Priced Timed Automata
 Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks
 Isbn
 9783540445852
 Label
 Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 1822, 2001 : proceedings
 Title
 Computer aided verification
 Title remainder
 13th International conference, CAV 2001, Paris, France, July 1822, 2001 : proceedings
 Statement of responsibility
 Gérard Berry, Hubert Comon, Alain Finkel (eds.)
 Title variation
 CAV 2001
 Subject

 Computer software  Verification
 Computer software  Verification  Congresses
 Conference papers and proceedings
 Conference papers and proceedings
 Integrated circuits  Verification
 Integrated circuits  Verification
 Integrated circuits  Verification  Congresses
 Computer software  Verification
 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
 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 1822, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.)
 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?  TransformationBased Verification Using Generalized Retiming  BDD and Decision Procedures  MetaBDDs: 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 FormulaDependent 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 TheoremProving 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 BDDBased Model Checker for Recursive Programs  Temporal Logics and Verification  Model Checking the World Wide Web?  Distributed Symbolic Model Checking for?Calculus  Tool Presentations: ModelChecking 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 WordLevel Abstraction  SDLcheck: A Model Checking Tool  EASN: Integrating ASN. 1 and Model Checking  Rtdt: A FrontEnd for Efficient Model Checking of Synchronous Timing Diagrams  TAXYS: A Tool for the Development and Verification of RealTime 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  JobShop Scheduling Using Timed Automata?  As Cheap as Possible: Effcient CostOptimal 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/3540445854
 9783540423454
 http://library.link/vocab/ext/overdrive/overdriveId
 3540423451
 Sound
 unknown sound
 Specific material designation
 remote
 System control number
 (OCoLC)213933854
 Label
 Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 1822, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.)
 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?  TransformationBased Verification Using Generalized Retiming  BDD and Decision Procedures  MetaBDDs: 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 FormulaDependent 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 TheoremProving 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 BDDBased Model Checker for Recursive Programs  Temporal Logics and Verification  Model Checking the World Wide Web?  Distributed Symbolic Model Checking for?Calculus  Tool Presentations: ModelChecking 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 WordLevel Abstraction  SDLcheck: A Model Checking Tool  EASN: Integrating ASN. 1 and Model Checking  Rtdt: A FrontEnd for Efficient Model Checking of Synchronous Timing Diagrams  TAXYS: A Tool for the Development and Verification of RealTime 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  JobShop Scheduling Using Timed Automata?  As Cheap as Possible: Effcient CostOptimal 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/3540445854
 9783540423454
 http://library.link/vocab/ext/overdrive/overdriveId
 3540423451
 Sound
 unknown sound
 Specific material designation
 remote
 System control number
 (OCoLC)213933854
Subject
 Computer software  Verification
 Computer software  Verification  Congresses
 Conference papers and proceedings
 Conference papers and proceedings
 Integrated circuits  Verification
 Integrated circuits  Verification
 Integrated circuits  Verification  Congresses
 Computer software  Verification
Genre
Member of
 Lecture notes in computer science, Lecture notes in artificial intelligence
 Lecture notes in computer science, 2102
 Lecture notes in computer science, 2102.
Library Links
Embed
Settings
Select options that apply then copy and paste the RDF/HTML data fragment to include in your application
Embed this data in a secure (HTTPS) page:
Layout options:
Include data citation:
<div class="citation" vocab="http://schema.org/"><i class="fa faexternallinksquare fafw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Computeraidedverification13thInternational/u2hbAsrWKJc/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.library.missouri.edu/portal/Computeraidedverification13thInternational/u2hbAsrWKJc/">Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 1822, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.library.missouri.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.library.missouri.edu/">University of Missouri Libraries</a></span></span></span></span></div>
Note: Adjust the width and height settings defined in the RDF/HTML code fragment to best match your requirements
Preview
Cite Data  Experimental
Data Citation of the Item Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 1822, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.)
Copy and paste the following RDF/HTML data fragment to cite this resource
<div class="citation" vocab="http://schema.org/"><i class="fa faexternallinksquare fafw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Computeraidedverification13thInternational/u2hbAsrWKJc/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.library.missouri.edu/portal/Computeraidedverification13thInternational/u2hbAsrWKJc/">Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 1822, 2001 : proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.library.missouri.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.library.missouri.edu/">University of Missouri Libraries</a></span></span></span></span></div>