Borrow it
 African Studies Library
 Alumni Medical Library
 Astronomy Library
 Fineman and Pappas Law Libraries
 Frederick S. Pardee Management Library
 Howard Gotlieb Archival Research Center
 Mugar Memorial Library
 Music Library
 Pikering Educational Resources Library
 School of Theology Library
 Science & Engineering Library
 Stone Science Library
The Resource Computer Aided Verification : 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings, edited by Gérard Berry, Hubert Comon, Alain Finkel, (electronic resource)
Computer Aided Verification : 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings, edited by Gérard Berry, Hubert Comon, Alain Finkel, (electronic resource)
Resource Information
The item Computer Aided Verification : 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings, edited by Gérard Berry, Hubert Comon, Alain Finkel, (electronic resource) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in Boston University Libraries.This item is available to borrow from all library branches.
Resource Information
The item Computer Aided Verification : 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings, edited by Gérard Berry, Hubert Comon, Alain Finkel, (electronic resource) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in Boston University Libraries.
This item is available to borrow from all library branches.
 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
 XIII, 522 p.
 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 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
 edited by Gérard Berry, Hubert Comon, Alain Finkel
 Subject

 Software engineering
 Computer science
 Computer science
 Artificial intelligence
 Software engineering
 Logic Design
 Logic design
 Mathematical Logic and Formal Languages
 Computer Science
 Special Purpose and ApplicationBased Systems
 Computer Science
 Artificial intelligence
 Electronic resources
 Software engineering
 Artificial intelligence
 Logics and Meanings of Programs
 Logic design
 Computer Science
 Logic Design
 Computer science
 Artificial Intelligence (incl. Robotics)
 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
 http://library.link/vocab/creatorName
 Berry, Gérard
 Image bit depth
 0
 LC call number

 QA76.9.L63
 QA76.5913
 QA76.63
 Literary form
 non fiction
 http://library.link/vocab/relatedWorkOrContributorName

 Comon, Hubert.
 Finkel, Alain.
 SpringerLink
 Series statement
 Lecture Notes in Computer Science,
 Series volume
 2102
 http://library.link/vocab/subjectName

 Computer science
 Logic design
 Software engineering
 Artificial intelligence
 Computer Science
 Logics and Meanings of Programs
 Mathematical Logic and Formal Languages
 Artificial Intelligence (incl. Robotics)
 Special Purpose and ApplicationBased Systems
 Logic Design
 Label
 Computer Aided Verification : 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings, edited by Gérard Berry, Hubert Comon, Alain Finkel, (electronic resource)
 Antecedent source
 mixed
 Carrier category
 online resource
 Carrier category code
 cr
 Carrier MARC source
 rdacarrier
 Color
 not applicable
 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
 Dimensions
 unknown
 Extent
 XIII, 522 p.
 File format
 multiple file formats
 Form of item
 electronic
 Isbn
 9783540445852
 Level of compression
 uncompressed
 Media category
 computer
 Media MARC source
 rdamedia
 Media type code
 c
 Other control number
 10.1007/3540445854
 Other physical details
 online resource.
 Quality assurance targets
 absent
 Reformatting quality
 access
 Specific material designation
 remote
 System control number
 (DEHe213)9783540445852
 Label
 Computer Aided Verification : 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings, edited by Gérard Berry, Hubert Comon, Alain Finkel, (electronic resource)
 Antecedent source
 mixed
 Carrier category
 online resource
 Carrier category code
 cr
 Carrier MARC source
 rdacarrier
 Color
 not applicable
 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
 Dimensions
 unknown
 Extent
 XIII, 522 p.
 File format
 multiple file formats
 Form of item
 electronic
 Isbn
 9783540445852
 Level of compression
 uncompressed
 Media category
 computer
 Media MARC source
 rdamedia
 Media type code
 c
 Other control number
 10.1007/3540445854
 Other physical details
 online resource.
 Quality assurance targets
 absent
 Reformatting quality
 access
 Specific material designation
 remote
 System control number
 (DEHe213)9783540445852
Subject
 Artificial Intelligence (incl. Robotics)
 Artificial intelligence
 Artificial intelligence
 Artificial intelligence
 Computer Science
 Computer Science
 Computer Science
 Computer science
 Computer science
 Computer science
 Electronic resources
 Logic Design
 Logic Design
 Logic design
 Logic design
 Logics and Meanings of Programs
 Mathematical Logic and Formal Languages
 Software engineering
 Software engineering
 Software engineering
 Special Purpose and ApplicationBased Systems
Member of
Library Locations

African Studies LibraryBorrow it771 Commonwealth Avenue, 6th Floor, Boston, MA, 02215, US42.350723 71.108227


Astronomy LibraryBorrow it725 Commonwealth Avenue, 6th Floor, Boston, MA, 02445, US42.350259 71.105717

Fineman and Pappas Law LibrariesBorrow it765 Commonwealth Avenue, Boston, MA, 02215, US42.350979 71.107023

Frederick S. Pardee Management LibraryBorrow it595 Commonwealth Avenue, Boston, MA, 02215, US42.349626 71.099547

Howard Gotlieb Archival Research CenterBorrow it771 Commonwealth Avenue, 5th Floor, Boston, MA, 02215, US42.350723 71.108227


Music LibraryBorrow it771 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US42.350723 71.108227

Pikering Educational Resources LibraryBorrow it2 Silber Way, Boston, MA, 02215, US42.349804 71.101425

School of Theology LibraryBorrow it745 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US42.350494 71.107235

Science & Engineering LibraryBorrow it38 Cummington Mall, Boston, MA, 02215, US42.348472 71.102257

Embed (Experimental)
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.bu.edu/portal/ComputerAidedVerification13thInternational/WPXkRifg4C8/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.bu.edu/portal/ComputerAidedVerification13thInternational/WPXkRifg4C8/">Computer Aided Verification : 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings, edited by Gérard Berry, Hubert Comon, Alain Finkel, (electronic resource)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.bu.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.bu.edu/">Boston University 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 18–22, 2001 Proceedings, edited by Gérard Berry, Hubert Comon, Alain Finkel, (electronic resource)
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.bu.edu/portal/ComputerAidedVerification13thInternational/WPXkRifg4C8/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.bu.edu/portal/ComputerAidedVerification13thInternational/WPXkRifg4C8/">Computer Aided Verification : 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings, edited by Gérard Berry, Hubert Comon, Alain Finkel, (electronic resource)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.bu.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.bu.edu/">Boston University Libraries</a></span></span></span></span></div>