Computer Aided Verification

1. Front Matter

   PDF

2. Multipliers and dividers: Insights on arithmetic circuit verification (extended abstract)

   • Randal E. Bryant

   Pages 1-3

3. Global rebuilding of OBDDs avoiding memory requirement maxima

   • Jochen Bern, Christoph Meinel, Anna Slobodová

   Pages 4-15

4. Generating BDD models for process algebra terms

   • Ashvin Dsouza, Bard Bloom

   Pages 16-30

5. Hardware verification using monadic second-order logic

   • David A. Basin, Nils Klarlund

   Pages 31-41

6. Verifying safety properties of a class of infinite-state distributed algorithms

   • Bengt Jonsson, Lars Kempe

   Pages 42-53

7. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving

   • Jürgen Dingel, Thomas Filkorn

   Pages 54-69

8. CAVEAT: technique and tool for computer aided verification and transformation

   • E. Pascal Gribomont, Didier Rossetto

   Pages 70-83

9. An integration of model checking with automated proof checking

   • S. Rajan, N. Shankar, M. K. Srivas

   Pages 84-97

10. Automatic datapath abstraction in hardware systems

    • Ramin Hojati, Robert K. Brayton

    Pages 98-113

11. Toupie=μ-calculus+constraints

    • Antoine Rauzy

    Pages 114-126

12. Safety property verification of Esterel programs and applications to telecommunications software

    • Lalita Jategaonkar Jagadeesan, Carlos Puchol, James E. Von Olnhausen

    Pages 127-140

13. Methods for Mu-calculus model checking: A tutorial

    • E. A. Emerson

    Pages 141-141

14. Efficient checking of behavioural relations and modal assertions using fixed-point inversion

    • Henrik Reif Andersen, Bart Vergauwen

    Pages 142-154

15. It usually works: The temporal logic of stochastic systems

    • Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli

    Pages 155-165

16. Local liveness for compositional modeling of fair reactive systems

    • Rajeev Alur, Thomas A. Henzinger

    Pages 166-179

17. Trace theoretic verification of asynchronous circuits using unfoldings

    • K. L. McMillan

    Pages 180-195

18. From duration calculus to linear hybrid automata

    • Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana

    Pages 196-210

19. Local model checking for real-time systems

    • Oleg V. Sokolsky, Scott A. Smolka

    Pages 211-224

20. Algorithmic analysis of nonlinear hybrid systems

    • Thomas A. Henzinger, Pei -Hsin Ho

    Pages 225-238

This volume constitutes the proceedings of the 7th International Conference on Computer Aided Verification, CAV '95, held in Liège, Belgium in July 1995.
The book contains the 31 refereed full research papers selected for presentation at CAV '95 as well as abstracts or full papers of the three invited presentations. Originally oriented towards finite-state concurrent systems, CAV now covers all styles of verification approaches and a variety of application areas. The papers included range from theoretical issues to concrete applications with a certain emphasis on verification tools and the algorithms and techniques needed for their implementations. Beyond finite-state systems, real-time systems and hybrid systems are an important part of the conference.

• Computer Aided Verification
• Computergestützte Verifikation
• Echtzei-Systeme
• Endliche Systeme
• Finite-State Systems
• Formale Verifikationstechniken
• Hardware
• Rreal Time Systems
• System
• algorithms
• automata
• hardware verification
• logic
• modeling
• real-time

Policies and ethics