Skip to main content
SpringerLink
Log in
Book cover

Computer Aided Verification

12th International Conference, CAV 2000 Chicago, IL, USA, July 15-19, 2000 Proceedings

  • Conference proceedings
  • © 2000

Overview

Editors:
  1. E. Allen Emerson

    1. Aiken Computation Laboratory, Harvard University, Cambridge, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Aravinda Prasad Sistla

    1.  ,  

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 1855)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (48 papers)

  1. Front Matter

    Download chapter PDF

  3. Regular Papers

    1. An Abstraction Algorithm for the Verification of Generalized C-Slow Designs

      • Jason Baumgartner, Anson Tripp, Adnan Aziz, Vigyan Singhal, Flemming Andersen
      Pages 5-19

    2. Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits

      • Tamir Heyman, Danny Geist, Orna Grumberg, Assaf Schuster
      Pages 20-35

    3. An Automata-Theoretic Approach to Reasoning about Infinite-State Systems

      • Orna Kupferman, Moshe Y. Vardi
      Pages 36-52

    4. Automatic Verification of Parameterized Cache Coherence Protocols

      • Giorgio Delzanno
      Pages 53-68

    5. Binary Reachability Analysis of Discrete Pushdown Timed Automata

      • Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, Jianwen Su
      Pages 69-84

    6. Boolean Satisfiability with Transitivity Constraints

      • Randal E. Bryant, Miroslav N. Velev
      Pages 85-98

    7. Bounded Model Construction for Monadic Second-Order Logics

      • Abdelwaheb Ayari, David Basin
      Pages 99-112

    8. Building Circuits from Relations

      • James H. Kukula, Thomas R. Shiple
      Pages 113-123

    9. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking

      • Poul F. Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta
      Pages 124-138

    10. On the Completeness of Compositional Reasoning

      • Kedar S. Namjoshi, Richard J. Trefler
      Pages 139-153

    11. Counterexample-Guided Abstraction Refinement

      • Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
      Pages 154-169

    12. Decision Procedures for Inductive Boolean Functions Based on Alternating Automata

      • Abdelwaheb Ayari, David Basin, Felix Klaedtke
      Pages 170-185

    13. Detecting Errors Before Reaching Them

      • Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang
      Pages 186-201

    14. A Discrete Strategy Improvement Algorithm for Solving Parity Games

      • Jens Vöge, Marcin Jurdziński
      Pages 202-215

    15. Distributing Timed Model Checking — How the Search Order Matters

      • Gerd Behrmann, Thomas Hune, Frits Vaandrager
      Pages 216-231
Back to top

Keywords

About this book

This volume contains the proceedings of the 12th International Conference on Computer Aided Veri?cation (CAV 2000) held in Chicago, Illinois, USA during 15-19 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 usingthe 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 andforward-lookingcompaniesandorganizationsincluding: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).

Editors and Affiliations

  • Aiken Computation Laboratory, Harvard University, Cambridge, USA

    E. Allen Emerson

  •  ,  

    Aravinda Prasad Sistla

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation