Computer Aided Verification

1. Front Matter

   Pages I-XIII

   PDF

2. Invited Talks

   1. Software Analysis and Model Checking

      • Gerard_J. Holzmann

      Pages 1-16

   2. The Quest for Efficient Boolean Satisfiability Solvers

      • Lintao Zhang, Sharad Malik

      Pages 17-36

3. Invited Tutorials

   1. On Abstraction in Software Verification

      • Patrick Cousot, Radhia Cousot

      Pages 37-56

   2. The Symbolic Approach to Hybrid Systems

      • Thomas A. Henzinger

      Pages 57-57

   3. Infinite Games and Verification

      • Wolfgang Thomas

      Pages 58-65

4. Symbolic Model Checking

   1. Symbolic Localization Reduction with Reconstruction Layering and Backtracking

      • Sharon Barner, Daniel Geist, Anna Gringauze

      Pages 65-77

   2. Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions

      • Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia

      Pages 78-92

   3. Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking

      • Sharon Barner, Orna Grumberg

      Pages 93-106

5. Abstraction/Refinement and Model Checking

   1. Liveness with (0,1, ∞)- Counter Abstraction

      • Amir Pnueli, Jessie Xu, Lenore Zuck

      Pages 107-122

   2. Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking

      • Prosenjit Chatterjee, Hemanthkumar Sivaraj, Ganesh Gopalakrishnan

      Pages 123-136

   3. Automatic Abstraction Using Generalized Model Checking

      • Patrice Godefroid, Radha Jagadeesan

      Pages 137-151

6. Compositional/Structural Verification

   1. Property Checking via Structural Analysis

      • Jason Baumgartner, Andreas Kuehlmann, Jacob Abraham

      Pages 151-165

   2. Conformance Checking for Models of Asynchronous Message Passing Software

      • Sriram K. Rajamani, Jakob Rehof

      Pages 166-179

   3. A Modular Checker for Multithreaded Programs

      • Cormac Flanagan, Shaz Qadeer, Sanjit A. Seshia

      Pages 180-194

7. Timing Analysis

   1. Automatic Derivation of Timing Constraints by Failure Analysis

      • Tomohiro Yoneda, Tomoya Kitai, Chris Myers

      Pages 195-208

   2. Deciding Separation Formulas with SAT

      • Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant

      Pages 209-222

   3. Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling

      • Håkan L. S. Younes, Reid G. Simmons

      Pages 223-235

8. SAT Based Methods

   1. Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT

      • Clark W. Barrett, David L. Dill, Aaron Stump

      Pages 236-249

   2. Applying SAT Methods in Unbounded Symbolic Model Checking

      • Ken L. McMillan

      Pages 250-264

This volume contains the proceedings of the conference on Computer Aided V- i?cation (CAV 2002), held in Copenhagen, Denmark on July 27-31, 2002. CAV 2002 was the 14th in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical - sults to concrete applications, with an emphasis on practical veri?cation tools, including algorithms and techniques needed for their implementation. The c- ference has traditionally drawn contributions from researchers as well as prac- tioners in both academia and industry. This year we received 94 regular paper submissions out of which 35 were selected. Each submission received an average of 4 referee reviews. In addition, the CAV program contained 11 tool presentations selected from 16 submissions. For each tool presentation, a demo was given at the conference. The large number of tool submissions and presentations testi?es to the liveliness of the ?eld and its applied ?avor.

• Erfüllbarkeitsproblem der Aussagenlogik
• Formal methods
• automated deduction
• computational logic
• formal verification
• hardware verification
• learning
• machine learning
• model checking
• modeling
• petri net
• proving
• systems analysis
• theorem proving
• verification tools

• Department of Computer Science, University of Twente, Enschede, The Netherlands

  Ed Brinksma

• Department of Computer Science, Aalborg University, Aalborg Ø, Denmark

  Kim Guldstrand Larsen

Policies and ethics