4. CAV 1992: Montreal, Canada

Invited Lecture

• Leslie Lamport:
  Computer-Hindered Verification (Humans Can Do It Too). 1
  

Session: Reduction Techniques 1

• Hana De-Leon, Orna Grumberg:
  Modular Abstractions for Verifying Real-Time Distributed Systems. 2-15
  
• Mannes Poel, Job Zwiers:
  Layering Techniques for Development of Parallel Systems. 16-29
  
• Kim Guldstrand Larsen:
  Efficient Local Correctness Checking. 30-43
  

Session: Proof Checking

• Urban Engberg, Peter Grønning, Leslie Lamport:
  Mechanical Verification of Concurrent Systems with TLA. 44-55
  
• Joakim von Wright, Thomas Långbacka:
  Using a Theorem Prover for Reasoning about Concurrent Algorithms. 56-68
  
• Mark Aagaard, Miriam Leeser:
  Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification. 69-81
  

Session: Symbolic Verification 1

• Alan J. Hu, David L. Dill, Andreas J. Drexler, C. Han Yang:
  Higher-Level Specification and Verification with BDDs. 82-95
  
• Amar Bouali, Robert de Simone:
  Symbolic Bisimulation Minimisation. 96-108
  
• Prabhat Jain, Prabhakar Kudva, Ganesh Gopalakrishnan:
  Towards a Verification Technique for Large Synchronous Circuits. 109-122
  

Session: Timing Verification 1

• David K. Probst, Hon F. Li:
  Verifying Timed Behavior Automata with Nonbinary Delay Constraints. 123-136
  
• Rajeev Alur, Alon Itai, Robert P. Kurshan, Mihalis Yannakakis:
  Timing Verification by Successive Approximation. 137-150
  
• Felice Balarin, Alberto L. Sangiovanni-Vincentelli:
  A Verification Strategy for Timing-Constrained Systems. 151-163
  

Session: Partial-Order Approaches

• Kenneth L. McMillan:
  Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. 164-177
  
• Patrice Godefroid, Gerard J. Holzmann, Didier Pirottin:
  State-Space Caching Revisited. 178-191
  

Session: Case Studies

• Siegfried Fischer, Andreas Scholz, Dirk Taubner:
  Verification in Process Algebra of the Distributed Control of Track Vehicles - A Case Study. 192-205
  
• Kiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yajima:
  Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic. 206-219
  
• Glenn Bruns:
  A Case Study in Safety-Critical Design. 220-233
  

Session: Reduction Techniques 2

• Thomas R. Shiple, Massimiliano Chiodo, Alberto L. Sangiovanni-Vincentelli, Robert K. Brayton:
  Automatic Reduction in CTL Compositional Model Checking. 234-247
  
• Roope Kaivola:
  Compositional Model Checking for Linear-Time Temporal Logic. 248-259
  
• Saddek Bensalem, Ahmed Bouajjani, Claire Loiseaux, Joseph Sifakis:
  Property Preserving Simulations. 260-273
  

Session: Timing Verification 2

• Costas Courcoubetis, David L. Dill, Magda Chatzaki, Panagiotis Tzounakis:
  Verification with Real-Time COSPAN. 274-287
  
• Nathalie Rico, Gregor von Bochmann, Omar Cherkaoui:
  Model-Checking for Real-Time Systems Specified in Lotos. 288-301
  
• Karlis Cerans:
  Decidability of Bisimulation Equivalences for Parallel Timer Processes. 302-315
  

Session: Model and Proof Checking

• Julian C. Bradfield:
  A Proof Assistant for Symbolic Model-Checking. 316-329
  
• Angelika Mader:
  Tableau Recycling. 330-342
  
• Dominique Méry, Abdelillah Mokkedem:
  Crocos: An Integrated Environment for Interactive Verification of SDL Specifications. 343-356
  

Session: Other Approaches

• James C. Corbett:
  Verifying General Safety and Liveness Propterties with Integer Programming. 357-369
  
• Ufuk Celikkan, Rance Cleaveland:
  Generating Diagnostic Information for Behavioral Preorders. 370-383
  
• Masahiro Higuchi, Osamu Shirakawa, Hiroyuki Seki, Mamoru Fujii, Tadao Kasami:
  A Verification Procedure via Invariant for Extended Communicating Finite-State Machines. 384-395
  

Session: Symbolic Verification 2

• Ramin Hojati, Hervé J. Touati, Robert P. Kurshan, Robert K. Brayton:
  Efficient omega-Regular Language Containment. 396-409
  
• Rance Cleaveland, Marion Klein, Bernhard Steffen:
  Faster Model Checking for the Modal Mu-Calculus. 410-422