Computer Aided Verification

1. Front Matter

   PDF

2. Logic synthesis and design verification

   • Robert K. Brayton

   Pages 1-2

3. Efficient verification with BDDs using implicitly conjoined invariants

   • Alan J. Hu, David L. Dill

   Pages 3-14

4. Parametric circuit representation using inductive Boolean functions

   • Aarti Gupta, Allan L. Fisher

   Pages 15-28

5. An iterative approach to language containment

   • Felice Balarin, Alberto L. Sangiovanni-Vincentelli

   Pages 29-40

6. BDD-Based debugging of designs using language containment and fair CTL

   • Ramin Hojati, Robert K. Brayton, Robert P. Kurshan

   Pages 41-58

7. Reliable hashing without collision detection

   • Pierre Wolper, Denis Leroy

   Pages 59-70

8. A tool for symbolic program verification and abstraction

   • Susanne Graf, Claire Loiseaux

   Pages 71-84

9. Symbolic equivalence checking

   • J. C. Fernandez, A. Kerbrat, L. Mounier

   Pages 85-96

10. A decision algorithm for full propositional temporal logic

    • Y. Kesten, Z. Manna, H. McGuire, A. Pnueli

    Pages 97-109

11. Reachability and recurrence in Extended Finite State Machines: Modular Vector Addition Systems

    • A. S. Krishnakumar

    Pages 110-122

12. Automatic generation of network invariants for the verification of iterative sequential systems

    • June-Kyung Rho, Fabio Somenzi

    Pages 123-137

13. A Graphical Interval Logic toolset for verifying concurrent systems

    • G. Kutty, Y. S. Ramakrishna, L. E. Moser, L. K. Dillon, P. M. Melliar-Smith

    Pages 138-153

14. Combining model checking and theorem proving to verify parallel processes

    • Hardi Hungar

    Pages 154-165

15. Verification of a multiplier: 64 bits and beyond

    • R. P. Kurshan, Leslie Lamport

    Pages 166-179

16. Protocol design for an automated highway system

    • Pravin Varaiya

    Pages 180-180

17. Computing accumulated delays in real-time systems

    • Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger

    Pages 181-193

18. Reachability analysis of planar multi-linear systems

    • Oded Maler, Amir Pnueli

    Pages 194-209

19. An efficient algorithm for minimizing real-time transition systems

    • Mihalis Yannakakis, David Lee

    Pages 210-224

20. Verification of timing properties of VHDL

    • Costas Courcoubetis, Werner Damm, Bernhard Josko

    Pages 225-236

This volume contains the proceedings of the Fifth Conference on Computer-Aided Verfication, held in Crete, Greece, in June/July 1993. The objective of the CAV conferences is to bring together researchers and practitioners interested in the development anduse of methods, tools, and theories for the computer-aided verification of concurrent systems. The conferences provide an opportunity for comparing various verfication methods and tools that can be used to assist the applications designer. Emphasis is placed on new research results and the application of existing methods to real verification problems. The volume contains abstracts of three invited lectures and full versions of 37 contributed papers selected from 84 submissions.The contributions are grouped into sections on hardware verification with BDDs, methods and tools, theorem proving, analysis of real-time systems, processalgebras and calculi, partial orders, and exploiting symmetry.

• Addition
• Automatic Verification
• Boolean function
• Echtzeit-Systeme
• Equivalence
• Hardware
• Model Checking
• Process Algebras
• Prozessalgebren
• Real-Time Systems
• algorithms
• automata
• calculus
• formal verification
• verification

Policies and ethics