Computer Aided Verification

1. Front Matter

   PDF

2. Practical challenges for industrial formal verification tools

   • F. Erich Marschner

   Pages 1-2

3. Formal verification of digital systems, from ASICs to HW/SW codesign — a pragmatic approach

   • Roger B. Hughes

   Pages 3-6

4. The industrial success of verification tools based on stålmarck's method

   • Arne Borälv

   Pages 7-10

5. Formal verification — Applications & case studies

   • Martin Rowe

   Pages 11-11

6. Automatic abstraction techniques for propositional μ-calculus model checking

   • Abelardo Pardo, Gary D. Hachtel

   Pages 12-23

7. A compositional rule for hardware design refinement

   • K. L. McMillan

   Pages 24-35

8. Module checking revisited

   • Orna Kupferman, Moshe Y. Vardi

   Pages 36-47

9. Using compositional preorders in the verification of sliding window protocol

   • Roope Kaivola

   Pages 48-59

10. An efficient decision procedure for the theory of fixed-sized bit-vectors

    • David Cyrluk, Oliver Möller, Harald Rueß

    Pages 60-71

11. Construction of abstract state graphs with PVS

    • Susanne Graf, Hassen Saidi

    Pages 72-83

12. Verification of a chemical process leak test procedure

    • Adam L. Turk, Scott T. Probst, Gary J. Powers

    Pages 84-94

13. Automatic datapath extraction for efficient usage of HDD

    • Gila Kamhi, Osnat Weissberg, Limor Fix, Ziv Binyamini, Ze'ev Shtadler

    Pages 95-106

14. An n log n algorithm for online BDD refinement

    • Nils Klarlund

    Pages 107-118

15. Weak bisimulation for fully probabilistic processes

    • Christel Baier, Holger Hermanns

    Pages 119-130

16. Towards a mechanization of cryptographic protocol verification

    • Dominique Bolignano

    Pages 131-142

17. Efficient model checking using tabled resolution

    • Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David S. Warren

    Pages 143-154

18. Containment of regular languages in non-regular timing diagram languages is decidable

    • Kathi Fisler

    Pages 155-166

19. An improved reachability analysis method for strongly linear hybrid systems (extended abstract)

    • Bernard Boigelot, Louis Bronne, Stéphane Rassart

    Pages 167-178

20. Some progress in the symbolic verification of timed automata

    • Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine

    Pages 179-190

This book constitutes the strictly refereed proceedings of the 9th International Conference on Computer Aided Verification, CAV '97, held in Haifa, Israel, in June 1997.
The volume presents 34 revised full papers selected from a total of 84 submissions. Also included are 7 invited contributions as well as 12 tool descriptions. The volume is dedicated to the theory and practice of computer aided formal methods for software and hardware verification, with an emphasis on verification tools and algorithms and the techniques needed for their implementation. The book is a unique record documenting the recent progress in the area.

• Hardware
• algorithm
• algorithms
• computer
• formal method
• hardware verification
• tools
• verification

Policies and ethics