2. CAV 1990: New Brunswick, NJ, USA

• Edmund M. Clarke:
  Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem. 1
  

1. Tools and Computation

• Hans Eveking:
  Automatic Verification of Extensions of Hardware Descriptions. 2-12
  
• Gérard Berthelot, Colette Johnen, Laure Petrucci:
  PAPETRI: Environment for the Analysis of Petri Nets. 13-22
  
• Olivier Coudert, Jean Christophe Madre, Christian Berthet:
  Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams. 23-32
  
• Randal E. Bryant, Carl-Johan H. Seger:
  Formal Verification of Digital Circuits Using Symbolic Ternary System Models. 33-43
  
• Hiromi Hiraishi, Shintaro Meki, Kiyoharu Hamaguchi:
  Vectorized Model Checking for Computation Tree Logic. 44-53
  
• Carl Pixley:
  Introduction to a Computational Theory and Implementation of Sequential Hardware Equivalence. 54-64
  
• Valérie Roy, Robert de Simone:
  Auto/Autograph. 65-75
  
• Hiroshi Nakamura, Yuji Kukimoto, Masahiro Fujita, Hidehiko Tanaka:
  A Data Path Verifier for Register Transfer Level Using Temporal Logic Language Tokio. 76-85
  
• Paolo Camurati, M. Gilli, Paolo Prinetto, Matteo Sonza Reorda:
  The Use of Model Checking in ATPG for Sequential Circuits. 86-95
  
• Jean Christophe Lloret, Pierre Azéma, François Vernadat:
  Compositional Design and Verification of Communication Protocols, Using Labelled Petri Nets. 96-105
  
• Linda A. Ness:
  Issues Arising in the Analysis of L.0. 106-115
  
• Michel Langevin:
  Automated RTL Verification Based on Predicate Calculus. 116-125
  
• Richard Lai, Ken R. Parker, Tharam S. Dillon:
  On Using Protean To Verify ISO FTAM Protocol. 126-135
  
• E. Allen Emerson, Aloysius K. Mok, A. Prasad Sistla, Jai Srinivasan:
  Quantitative Temporal Reasoning. 136-145
  

2. Partial Orders

• David K. Probst, Hon F. Li:
  Using Partial-Order Semantics to Avoid the State Explosion Problem in Asynchronous Systems. 146-155
  
• Antti Valmari:
  A Stubborn Attack On State Explosion. 156-165
  
• Ryszard Janicki, Maciej Koutny:
  Using Optimal Simulations to Reduce Reachability Graphs. 166-175
  
• Patrice Godefroid:
  Using Partial Orders to Improve Automatic Verification Methods. 176-185
  

3. Reduction in Finite State Systems

• Susanne Graf, Bernhard Steffen:
  Compositional Minimization of Finite State Systems. 186-196
  
• Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs:
  Minimal Model Generation. 197-203
  
• Bernhard Josko:
  A Context Dependent Equivalence Relation Between Kripke Structures. 204-213
  
• Gil Shurek, Orna Grumberg:
  The Modular Framework of Computer-Aided Verification. 214-223
  

4. Automaton Models

• Jerry R. Burch:
  Verifying Liveness Properties by Verifying Safety Properties. 224-232
  
• Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, Mihalis Yannakakis:
  Memory Efficient Algorithms for the Verification of Temporal Properties. 233-242
  
• Wuxu Peng, S. Purushothaman:
  A Unified Approach to the Deadlock Detection Problem in Networks of Communicating Finite State Machines. 243-252
  
• Kiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yajima:
  Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity. 253-262
  
• Victor Yodaiken:
  The Algebraic Feedback Product of Automata. 263-271
  

5. Model Synthesis

• Howard Wong-Toi, David L. Dill:
  Synthesizing Processes and Schedulers from Temporal Specifications. 272-281
  
• Christian H. Golaszewski, Robert P. Kurshan:
  Task-Driven Supervisory Control of Discrete Event Systems. 282-291
  
• Ugo A. Buy, Robert Moll:
  A Proof Lattice-Based Technique for Analyzing Liveness of Resource Controllers. 292-301
  

6. Theorem-Provers

• Paul Loewenstein, David L. Dill:
  Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic. 302-311
  
• David A. Carrington, K. A. Robinson:
  Computer Assistance for Program Refinement. 312-321
  
• James M. Morris, Mark Howard:
  Program Verification by Symbolic Execution of Hyperfinite Ideal Machines. 322-332
  

7. Process Algebra

• Michel Barbeau, Gregor von Bochmann:
  Extension of the Karp and Miller Procedure to Lotos Specifications. 333-342
  
• Mark B. Josephs, Jan Tijmen Udding:
  An Algebra for Delay-Insensitive Circuits. 343-352
  
• Eric Madelaine, Didier Vergamini:
  Finiteness Conditions and Structural Construction of Automata for All Process Algebras. 353-363
  
• Rance Cleaveland:
  On Automatically Explaining Bisimulation Inequivalence. 364-372