CAV 1990

38 papers

1. A Context Dependent Equivalence Relation Between Kripke Structures · Bernhard Josko
2. A Data Path Verifier for Register Transfer Level Using Temporal Logic Language Tokio · Hiroshi Nakamura, Yuji Kukimoto, Masahiro Fujita, Hidehiko Tanaka
3. A Proof Lattice-Based Technique for Analyzing Liveness of Resource Controllers · Ugo A. Buy, Robert Moll
4. A Stubborn Attack On State Explosion · Antti Valmari
5. A Unified Approach to the Deadlock Detection Problem in Networks of Communicating Finite State Machines · Wuxu Peng, S. Purushothaman
6. An Algebra for Delay-Insensitive Circuits · Mark B. Josephs, Jan Tijmen Udding
7. Auto/Autograph · Valérie Roy, Robert de Simone
8. Automated RTL Verification Based on Predicate Calculus · Michel Langevin
9. Automatic Verification of Extensions of Hardware Descriptions · Hans Eveking
10. Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity · Kiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yajima
11. Compositional Design and Verification of Communication Protocols, Using Labelled Petri Nets · Jean Christophe Lloret, Pierre Azéma, François Vernadat
12. Compositional Minimization of Finite State Systems · Susanne Graf, Bernhard Steffen
13. Computer Assistance for Program Refinement · David A. Carrington, Kenneth Arthur Robinson
14. Extension of the Karp and Miller Procedure to Lotos Specifications · Michel Barbeau, Gregor von Bochmann
15. Finiteness Conditions and Structural Construction of Automata for All Process Algebras · Eric Madelaine, Didier Vergamini
16. Formal Verification of Digital Circuits Using Symbolic Ternary System Models · Randal E. Bryant, Carl-Johan H. Seger
17. Introduction to a Computational Theory and Implementation of Sequential Hardware Equivalence · Carl Pixley
18. Issues Arising in the Analysis of L.0 · Linda A. Ness
19. Memory Efficient Algorithms for the Verification of Temporal Properties · Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, Mihalis Yannakakis
20. Minimal Model Generation · Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs
21. On Automatically Explaining Bisimulation Inequivalence · Rance Cleaveland
22. On Using Protean To Verify ISO FTAM Protocol · Richard Lai, Ken R. Parker, Tharam S. Dillon
23. PAPETRI: Environment for the Analysis of Petri Nets · Gérard Berthelot, Colette Johnen, Laure Petrucci
24. Program Verification by Symbolic Execution of Hyperfinite Ideal Machines · James M. Morris, Mark Howard
25. Quantitative Temporal Reasoning · E. Allen Emerson, Aloysius K. Mok, A. Prasad Sistla, Jai Srinivasan
26. Synthesizing Processes and Schedulers from Temporal Specifications · Howard Wong-Toi, David L. Dill
27. Task-Driven Supervisory Control of Discrete Event Systems · Christian H. Golaszewski, Robert P. Kurshan
28. Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem · Edmund M. Clarke
29. The Algebraic Feedback Product of Automata · Victor Yodaiken
30. The Modular Framework of Computer-Aided Verification · Gil Shurek, Orna Grumberg
31. The Use of Model Checking in ATPG for Sequential Circuits · Paolo Camurati, Marco Gilli, Paolo Prinetto, Matteo Sonza Reorda
32. Using Optimal Simulations to Reduce Reachability Graphs · Ryszard Janicki, Maciej Koutny
33. Using Partial Orders to Improve Automatic Verification Methods · Patrice Godefroid
34. Using Partial-Order Semantics to Avoid the State Explosion Problem in Asynchronous Systems · David K. Probst, Hon Fung Li
35. Vectorized Model Checking for Computation Tree Logic · Hiromi Hiraishi, Shintaro Meki, Kiyoharu Hamaguchi
36. Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic · Paul Loewenstein, David L. Dill
37. Verifying Liveness Properties by Verifying Safety Properties · Jerry R. Burch
38. Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams · Olivier Coudert, Jean Christophe Madre, Christian Berthet