Computer Aided Verification

1. Front Matter

   PDF

2. Taming infinite state spaces

   • Colin Sterling

   Pages 1-1

3. Silence is golden: Branching bisimilarity is decidable for context-free processes

   • Hans Hüttel

   Pages 2-12

4. Computing distinguishing formulas for branching bisimulation

   • Henri Korver

   Pages 13-23

5. Compositional checking of satisfaction

   • Henrik Reif Andersen, Glynn Winskel

   Pages 24-36

6. An action based framework for verifying logical and behavioural properties of concurrent systems

   • R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori

   Pages 37-47

7. A linear-time model-checking algorithm for the alternation-free modal mu-calculus

   • Ranee Cleaveland, Bernhard Steffen

   Pages 48-58

8. Automatic temporal verification of buffer systems

   • A. Prasad Sistla, Lenore D. Zuck

   Pages 59-69

9. Mechanically checked proofs of kernel specifications

   • William R. Bevier, JØrgen F. SØgaard-Andersen

   Pages 70-82

10. A top down approach to the formal specification of SCI cache coherence

    • Stein Gjessing, Stein Krogdahl, Ellen Munthe-Kaas

    Pages 83-91

11. Integer programming in the analysis of concurrent systems

    • George S. Avrunin, Ugo A. Buy, James C. Corbett

    Pages 92-102

12. The lotos model of a fault protected system and its verification using a petri net based approach

    • Michel Barbeau, Gregor v. Bochmann

    Pages 103-113

13. Error diagnosis in finite communicating systems

    • Anne Rasse

    Pages 114-124

14. Temporal precondition verification of design transformations

    • Ranga Vemuri, Anuradha Sridhar

    Pages 125-135

15. PAM: A process algebra manipulator

    • Huimin Lin

    Pages 136-146

16. The Concurrency Workbench with priorities

    • Claus Torp Jensen

    Pages 147-157

17. A proof assistant for PSF

    • S. Mauw, G. J. Veltink

    Pages 158-168

18. Avoiding state explosion by composition of minimal covering graphs

    • Alain Finkel, Laure Petrucci

    Pages 169-180

19. “On the fly” verification of behavioural equivalences and preorders

    • Jean -Claude Fernandez, Laurent Mounier

    Pages 181-191

20. Bounded-memory algorithms for verification on-the-fly

    • Claude Jard, Thierry Jéron

    Pages 192-202

This volume contains the proceedings of the third International Workshop on Computer Aided Verification, CAV '91, held in Aalborg, Denmark, July 1-4, 1991. The objective of this series of workshops is to bring together researchers and practitioners interested in the development and use of methods, tools and theories for automatic verification of (finite) state systems. The workshop provides a unique opportunity for comparing the numerous verification methods and associated verification tools, and the extent to which they may be utilized in application design. The emphasis is not only on new research results but also on the application of existing results to real verification problems. The papers in the volume areorganized into sections on equivalence checking, model checking, applications, tools for process algebras, the state explosion problem, symbolic model checking, verification and transformation techniques, higher order logic, partial order approaches, hardware verification, timed specification and verification, and automata.

• Automat
• automata
• computer
• logic
• model checking
• tools
• verification

Policies and ethics