Computer Aided Verification

1. Front Matter

   Pages I-XII

   PDF

2. Tutorials and Invited Papers

   1. Alternative Approaches to Hardware Verification

      • David L. Dill

      Pages 1-1

   2. The Compositional Specification of Timed Systems — A Tutorial

      • Joseph Sifakis

      Pages 2-7

   3. Timed Automata

      • Rajeev Alur

      Pages 8-22

   4. Ståalmarck’s Method with Extensions to Quantified Boolean Formulas

      • Gunnar Stålmarck

      Pages 23-24

   5. Verification of Parameterized Systems by Dynamic Induction

      • Zohar Manna, Henny B. Sipma

      Pages 25-43

   6. Formal Methods for Conformance Testing: Theory Can Be Practical

      • Ed Brinksma

      Pages 44-46

3. Processor Verification

   1. Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach

      • Ravi Hosabettu, Mandayam Srivas, Ganesh Gopalakrishnan

      Pages 47-59

   2. Verifying Safety Properties of a PowerPC− Microprocessor Using Symbolic Model Checking without BDDs

      • Armin Biere, Edmund Clarke, Richard Raimi, Yunshan Zhu

      Pages 60-71

   3. Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists

      • Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz

      Pages 72-83

   4. Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study

      • S. Ramesh, Purandar Bhaduri

      Pages 84-95

4. Protocol Verification and Testing

   1. Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol

      • Béeatrice Béerard, Laurent Fribourg

      Pages 96-107

   2. Test Generation Derived from Model-Checking

      • Thierry Jéron, Pierre Morel

      Pages 108-122

   3. Latency Insensitive Protocols

      • Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli

      Pages 123-133

5. Infinite State Space

   1. Handling Global Conditions in Parametrized System Verification

      • Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson

      Pages 134-145

   2. Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis

      • Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech

      Pages 146-159

   3. Experience with Predicate Abstraction

      • Satyaki Das, David L. Dill, Seungjoon Park

      Pages 160-171

6. Theory of Verification

   1. Model Checking of Safety Properties

      • Orna Kupferman, MosheY. Vardi

      Pages 172-183

   2. A Complete Finite Prefix for Process Algebra

      • Rom Langerak, Ed Brinksma

      Pages 184-195

   3. The Mathematical Foundation of Symbolic Trajectory Evaluation

      • Ching-Tsun Chou

      Pages 196-207

This book constitutes the refereed proceedings of the 11th International Conference on Computer Aided Verification, CAV'99, held in Trento, Italy in July 1999 as part of FLoC'99.
The 34 revised full papers presented were carefully reviewed and selected from a total of 107 submissions. Also included are six invited contributions and five tool presentations. The book is organized in topical sections on processor verification, protocol verification and testing, infinite state spaces, theory of verification, linear temporal logic, modeling of systems, symbolic model checking, theorem proving, automata-theoretic methods, and abstraction.

• Automat
• automata
• logic
• model checking
• modeling
• testing
• theorem proving
• verification

• Vérimag/CNRS, Gières, France

  Nicolas Halbwachs

• Bell Laboratories, Murray Hill, USA

  Doron Peled

• The Technion, Haifa, Israel

  Doron Peled

Policies and ethics