Computer Aided Verification

1. Front Matter

   PDF

2. Invited Talks and Tutorials

   1. Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion

      • Amir Pnueli

      Pages 1-1

   2. Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis

      • Catherine Meadows

      Pages 2-2

   3. Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation

      • João Marques-Silva, Karem Sakallah

      Pages 3-3

   4. Invited Tutorial: Verification of Infinite-state and Parameterized Systems

      • Parosh Aziz Abdulla, Bengt Jonsson

      Pages 4-4

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

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).

• Automated Deduction
• Formal Methods
• Hardware Verification
• Java
• Model Checking
• Program Verification
• Systems Analysis
• Systems Verification
• algorithm
• algorithms
• automata
• design
• formal verification
• programming
• verification

• Aiken Computation Laboratory, Harvard University, Cambridge, USA

  E. Allen Emerson

•  ,  

  Aravinda Prasad Sistla

Policies and ethics