Borrow it
 Architecture Library
 Bizzell Memorial Library
 Boorstin Collection
 Chinese Literature Translation Archive
 Engineering Library
 Fine Arts Library
 Harry W. Bass Business History Collection
 History of Science Collections
 John and Mary Nichols Rare Books and Special Collections
 Library Service Center
 Price College Digital Library
 Western History Collections
The Resource Computer Aided Verification : 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings, edited by E. Allen Emerson, A. Prasad Sistla, (electronic resource)
Computer Aided Verification : 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings, edited by E. Allen Emerson, A. Prasad Sistla, (electronic resource)
Resource Information
The item Computer Aided Verification : 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings, edited by E. Allen Emerson, A. Prasad Sistla, (electronic resource) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Oklahoma Libraries.This item is available to borrow from all library branches.
Resource Information
The item Computer Aided Verification : 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings, edited by E. Allen Emerson, A. Prasad Sistla, (electronic resource) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Oklahoma Libraries.
This item is available to borrow from all library branches.
 Summary
 This volume contains the proceedings of the 12th International Conference on Computer Aided Veri?cation (CAV 2000) held in Chicago, Illinois, USA during 1519 July 2000. The CAV conferences are devoted to the advancement of the theory and practice of formal methods for hardware and software veri?cation. The con rence covers the spectrum from theoretical foundations to concrete applications, with an emphasis on veri?cation algorithms, methods, and tools together with techniques for their implementation. The conference has traditionally drawn contributions from both researchers and practitioners in academia and industry. This year 91 regular research papers were submitted out of which 35 were  cepted, while 14 brief tool papers were submitted, out of which 9 were accepted for presentation. CAV included two invited talks and a panel discussion. CAV also included a tutorial day with two invited tutorials. Many industrial companies have shown a serious interest in CAV, ranging from using the presented technologies in their business to developing and m keting their own formal veri?cation tools. We are very proud of the support we receive from industry. CAV 2000 was sponsored by a number of generous andforwardlookingcompaniesandorganizationsincluding:CadenceDesign stems, IBM Research, Intel, Lucent Technologies, Mentor Graphics, the Minerva Center for Veri?cation of Reactive Systems, Siemens, and Synopsys. TheCAVconferencewasfoundedbyitsSteeringCommittee:EdmundClarke (CMU), Bob Kurshan (Bell Labs), Amir Pnueli (Weizmann), and Joseph Sifakis (Verimag)
 Language

 eng
 eng
 Edition
 1st ed. 2000.
 Extent
 1 online resource (X, 590 p.)
 Note
 Bibliographic Level Mode of Issuance: Monograph
 Contents

 Invited Talks and Tutorials
 Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion
 Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis
 Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation
 Invited Tutorial: Verification of Infinitestate and Parameterized Systems
 Regular Papers
 An Abstraction Algorithm for the Verification of Generalized CSlow Designs
 Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits
 An AutomataTheoretic Approach to Reasoning about InfiniteState Systems
 Automatic Verification of Parameterized Cache Coherence Protocols
 Binary Reachability Analysis of Discrete Pushdown Timed Automata
 Boolean Satisfiability with Transitivity Constraints
 Bounded Model Construction for Monadic SecondOrder Logics
 Building Circuits from Relations
 Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking
 On the Completeness of Compositional Reasoning
 CounterexampleGuided Abstraction Refinement
 Decision Procedures for Inductive Boolean Functions Based on Alternating Automata
 Detecting Errors Before Reaching Them
 A Discrete Strategy Improvement Algorithm for Solving Parity Games
 Distributing Timed Model Checking — How the Search Order Matters
 Efficient Algorithms for Model Checking Pushdown Systems
 Efficient Büchi Automata from LTL Formulae
 Efficient Detection of Global Properties in Distributed Systems Using PartialOrder Methods
 Efficient Reachability Analysis of Hierarchical Reactive Machines
 Formal Verification of VLIW Microprocessors with Speculative Execution
 Induction in Compositional Model Checking
 Liveness and Acceleration in Parameterized Verification
 Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm
 Model Checking ContinuousTime Markov Chains by Transient Analysis
 ModelChecking for Hybrid Systems by Quotienting and Constraints Solving
 Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification
 Regular Model Checking
 Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems
 Syntactic Program Transformations for Automatic Abstraction
 Temporallogic Queries
 Are Timed Automata Updatable?
 Tuning SAT Checkers for Bounded Model Checking
 Unfoldings of Unbounded Petri Nets
 Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification
 Verifying Advanced Microarchitectures that Support Speculation and Exceptions
 Tool Papers
 FoCs – Automatic Generation of Simulation Checkers from Formal Specifications
 IF: A Validation Environment for Timed Asynchronous Systems
 Integrating WS1S with PVS
 PET: An Interactive Software Testing Tool
 A ProofCarrying Code Architecture for Java
 The Statemate Verification Environment
 TAPS: A FirstOrder Verifier for Cryptographic Protocols
 VINASP: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits
 XMC: A LogicProgrammingBased Verification Toolset
 Isbn
 9783540450474
 Label
 Computer Aided Verification : 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings
 Title
 Computer Aided Verification
 Title remainder
 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings
 Statement of responsibility
 edited by E. Allen Emerson, A. Prasad Sistla
 Language

 eng
 eng
 Summary
 This volume contains the proceedings of the 12th International Conference on Computer Aided Veri?cation (CAV 2000) held in Chicago, Illinois, USA during 1519 July 2000. The CAV conferences are devoted to the advancement of the theory and practice of formal methods for hardware and software veri?cation. The con rence covers the spectrum from theoretical foundations to concrete applications, with an emphasis on veri?cation algorithms, methods, and tools together with techniques for their implementation. The conference has traditionally drawn contributions from both researchers and practitioners in academia and industry. This year 91 regular research papers were submitted out of which 35 were  cepted, while 14 brief tool papers were submitted, out of which 9 were accepted for presentation. CAV included two invited talks and a panel discussion. CAV also included a tutorial day with two invited tutorials. Many industrial companies have shown a serious interest in CAV, ranging from using the presented technologies in their business to developing and m keting their own formal veri?cation tools. We are very proud of the support we receive from industry. CAV 2000 was sponsored by a number of generous andforwardlookingcompaniesandorganizationsincluding:CadenceDesign stems, IBM Research, Intel, Lucent Technologies, Mentor Graphics, the Minerva Center for Veri?cation of Reactive Systems, Siemens, and Synopsys. TheCAVconferencewasfoundedbyitsSteeringCommittee:EdmundClarke (CMU), Bob Kurshan (Bell Labs), Amir Pnueli (Weizmann), and Joseph Sifakis (Verimag)
 Dewey number
 005.1
 http://bibfra.me/vocab/relation/httpidlocgovvocabularyrelatorsedt

 7fA9oqHyS0s
 1PVkA3nN6DE
 Image bit depth
 0
 Language note
 English
 LC call number
 QA76.758
 Literary form
 non fiction
 http://bibfra.me/vocab/lite/meetingName
 CAV (Conference)
 Nature of contents
 dictionaries
 http://library.link/vocab/relatedWorkOrContributorName

 Emerson, E. Allen.
 Sistla, A. Prasad.
 Series statement
 Lecture Notes in Computer Science,
 Series volume
 1855
 http://library.link/vocab/subjectName

 Software engineering
 Logic design
 Computer science
 Artificial intelligence
 Software Engineering/Programming and Operating Systems
 Logics and Meanings of Programs
 Software Engineering
 Mathematical Logic and Formal Languages
 Special Purpose and ApplicationBased Systems
 Artificial Intelligence
 Label
 Computer Aided Verification : 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings, edited by E. Allen Emerson, A. Prasad Sistla, (electronic resource)
 Note
 Bibliographic Level Mode of Issuance: Monograph
 Antecedent source
 mixed
 Bibliography note
 Includes bibliographical references at the end of each chapters and index
 Carrier category
 online resource
 Carrier category code

 cr
 Color
 not applicable
 Content category
 text
 Content type code

 txt
 Contents
 Invited Talks and Tutorials  Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion  Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis  Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation  Invited Tutorial: Verification of Infinitestate and Parameterized Systems  Regular Papers  An Abstraction Algorithm for the Verification of Generalized CSlow Designs  Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits  An AutomataTheoretic Approach to Reasoning about InfiniteState Systems  Automatic Verification of Parameterized Cache Coherence Protocols  Binary Reachability Analysis of Discrete Pushdown Timed Automata  Boolean Satisfiability with Transitivity Constraints  Bounded Model Construction for Monadic SecondOrder Logics  Building Circuits from Relations  Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking  On the Completeness of Compositional Reasoning  CounterexampleGuided Abstraction Refinement  Decision Procedures for Inductive Boolean Functions Based on Alternating Automata  Detecting Errors Before Reaching Them  A Discrete Strategy Improvement Algorithm for Solving Parity Games  Distributing Timed Model Checking — How the Search Order Matters  Efficient Algorithms for Model Checking Pushdown Systems  Efficient Büchi Automata from LTL Formulae  Efficient Detection of Global Properties in Distributed Systems Using PartialOrder Methods  Efficient Reachability Analysis of Hierarchical Reactive Machines  Formal Verification of VLIW Microprocessors with Speculative Execution  Induction in Compositional Model Checking  Liveness and Acceleration in Parameterized Verification  Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm  Model Checking ContinuousTime Markov Chains by Transient Analysis  ModelChecking for Hybrid Systems by Quotienting and Constraints Solving  Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification  Regular Model Checking  Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems  Syntactic Program Transformations for Automatic Abstraction  Temporallogic Queries  Are Timed Automata Updatable?  Tuning SAT Checkers for Bounded Model Checking  Unfoldings of Unbounded Petri Nets  Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification  Verifying Advanced Microarchitectures that Support Speculation and Exceptions  Tool Papers  FoCs – Automatic Generation of Simulation Checkers from Formal Specifications  IF: A Validation Environment for Timed Asynchronous Systems  Integrating WS1S with PVS  PET: An Interactive Software Testing Tool  A ProofCarrying Code Architecture for Java  The Statemate Verification Environment  TAPS: A FirstOrder Verifier for Cryptographic Protocols  VINASP: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits  XMC: A LogicProgrammingBased Verification Toolset
 Dimensions
 unknown
 Edition
 1st ed. 2000.
 Extent
 1 online resource (X, 590 p.)
 File format
 multiple file formats
 Form of item
 online
 Isbn
 9783540450474
 Level of compression
 uncompressed
 Media category
 computer
 Media type code

 c
 Other control number
 10.1007/10722167
 Quality assurance targets
 absent
 Reformatting quality
 access
 Specific material designation
 remote
 System control number

 (CKB)1000000000548803
 (SSID)ssj0000322073
 (PQKBManifestationID)11235585
 (PQKBTitleCode)TC0000322073
 (PQKBWorkID)10281158
 (PQKB)11466583
 (DEHe213)9783540450474
 (MiAaPQ)EBC3087407
 (EXLCZ)991000000000548803
 Label
 Computer Aided Verification : 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings, edited by E. Allen Emerson, A. Prasad Sistla, (electronic resource)
 Note
 Bibliographic Level Mode of Issuance: Monograph
 Antecedent source
 mixed
 Bibliography note
 Includes bibliographical references at the end of each chapters and index
 Carrier category
 online resource
 Carrier category code

 cr
 Color
 not applicable
 Content category
 text
 Content type code

 txt
 Contents
 Invited Talks and Tutorials  Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion  Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis  Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation  Invited Tutorial: Verification of Infinitestate and Parameterized Systems  Regular Papers  An Abstraction Algorithm for the Verification of Generalized CSlow Designs  Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits  An AutomataTheoretic Approach to Reasoning about InfiniteState Systems  Automatic Verification of Parameterized Cache Coherence Protocols  Binary Reachability Analysis of Discrete Pushdown Timed Automata  Boolean Satisfiability with Transitivity Constraints  Bounded Model Construction for Monadic SecondOrder Logics  Building Circuits from Relations  Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking  On the Completeness of Compositional Reasoning  CounterexampleGuided Abstraction Refinement  Decision Procedures for Inductive Boolean Functions Based on Alternating Automata  Detecting Errors Before Reaching Them  A Discrete Strategy Improvement Algorithm for Solving Parity Games  Distributing Timed Model Checking — How the Search Order Matters  Efficient Algorithms for Model Checking Pushdown Systems  Efficient Büchi Automata from LTL Formulae  Efficient Detection of Global Properties in Distributed Systems Using PartialOrder Methods  Efficient Reachability Analysis of Hierarchical Reactive Machines  Formal Verification of VLIW Microprocessors with Speculative Execution  Induction in Compositional Model Checking  Liveness and Acceleration in Parameterized Verification  Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm  Model Checking ContinuousTime Markov Chains by Transient Analysis  ModelChecking for Hybrid Systems by Quotienting and Constraints Solving  Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification  Regular Model Checking  Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems  Syntactic Program Transformations for Automatic Abstraction  Temporallogic Queries  Are Timed Automata Updatable?  Tuning SAT Checkers for Bounded Model Checking  Unfoldings of Unbounded Petri Nets  Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification  Verifying Advanced Microarchitectures that Support Speculation and Exceptions  Tool Papers  FoCs – Automatic Generation of Simulation Checkers from Formal Specifications  IF: A Validation Environment for Timed Asynchronous Systems  Integrating WS1S with PVS  PET: An Interactive Software Testing Tool  A ProofCarrying Code Architecture for Java  The Statemate Verification Environment  TAPS: A FirstOrder Verifier for Cryptographic Protocols  VINASP: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits  XMC: A LogicProgrammingBased Verification Toolset
 Dimensions
 unknown
 Edition
 1st ed. 2000.
 Extent
 1 online resource (X, 590 p.)
 File format
 multiple file formats
 Form of item
 online
 Isbn
 9783540450474
 Level of compression
 uncompressed
 Media category
 computer
 Media type code

 c
 Other control number
 10.1007/10722167
 Quality assurance targets
 absent
 Reformatting quality
 access
 Specific material designation
 remote
 System control number

 (CKB)1000000000548803
 (SSID)ssj0000322073
 (PQKBManifestationID)11235585
 (PQKBTitleCode)TC0000322073
 (PQKBWorkID)10281158
 (PQKB)11466583
 (DEHe213)9783540450474
 (MiAaPQ)EBC3087407
 (EXLCZ)991000000000548803
Subject
 Logic design
 Logics and Meanings of Programs
 Mathematical Logic and Formal Languages
 Software Engineering
 Software Engineering/Programming and Operating Systems
 Software engineering
 Special Purpose and ApplicationBased Systems
 Artificial Intelligence
 Artificial intelligence
 Computer science
Member of
Library Locations

Architecture LibraryBorrow itGould Hall 830 Van Vleet Oval Rm. 105, Norman, OK, 73019, US35.205706 97.445050



Chinese Literature Translation ArchiveBorrow it401 W. Brooks St., RM 414, Norman, OK, 73019, US35.207487 97.447906

Engineering LibraryBorrow itFelgar Hall 865 Asp Avenue, Rm. 222, Norman, OK, 73019, US35.205706 97.445050

Fine Arts LibraryBorrow itCatlett Music Center 500 West Boyd Street, Rm. 20, Norman, OK, 73019, US35.210371 97.448244

Harry W. Bass Business History CollectionBorrow it401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US35.207487 97.447906

History of Science CollectionsBorrow it401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US35.207487 97.447906

John and Mary Nichols Rare Books and Special CollectionsBorrow it401 W. Brooks St., Rm. 509NW, Norman, OK, 73019, US35.207487 97.447906


Price College Digital LibraryBorrow itAdams Hall 102 307 West Brooks St., Norman, OK, 73019, US35.210371 97.448244

Western History CollectionsBorrow itMonnet Hall 630 Parrington Oval, Rm. 300, Norman, OK, 73019, US35.209584 97.445414
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.libraries.ou.edu/portal/ComputerAidedVerification12thInternational/W_HepaRf3Ws/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.libraries.ou.edu/portal/ComputerAidedVerification12thInternational/W_HepaRf3Ws/">Computer Aided Verification : 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings, edited by E. Allen Emerson, A. Prasad Sistla, (electronic resource)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.libraries.ou.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.libraries.ou.edu/">University of Oklahoma 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 : 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings, edited by E. Allen Emerson, A. Prasad Sistla, (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.libraries.ou.edu/portal/ComputerAidedVerification12thInternational/W_HepaRf3Ws/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.libraries.ou.edu/portal/ComputerAidedVerification12thInternational/W_HepaRf3Ws/">Computer Aided Verification : 12th International Conference, CAV 2000 Chicago, IL, USA, July 1519, 2000 Proceedings, edited by E. Allen Emerson, A. Prasad Sistla, (electronic resource)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.libraries.ou.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.libraries.ou.edu/">University of Oklahoma Libraries</a></span></span></span></span></div>