6. CAV 1994: Stanford, California, USA

Real Time

• Rajeev Alur, Limor Fix, Thomas A. Henzinger:
  A Determinizable Class of Timed Automata. 1-13
  
• Roberto Gorrieri, Glauco Siliprandi:
  Real-Time System Verification using P/T Nets. 14-26
  
• William K. C. Lam, Robert K. Brayton:
  Criteria for the Simple Path Property in Timed Automata. 27-40
  

Symbolic Verification 1

• Kenneth L. McMillan:
  Hierarchical Representations of Discrete Functions, with Application to Model Checking. 41-54
  
• Bernard Boigelot, Pierre Wolper:
  Symbolic Verification with Periodic Sets. 55-67
  
• Jerry R. Burch, David L. Dill:
  Automatic verification of Pipelined Microprocessor Control. 68-80
  

Hybrid Systems

• Alfredo Olivero, Joseph Sifakis, Sergio Yovine:
  Using Abstractions for the Verification of Linear Hybrid Systems. 81-94
  
• Anuj Puri, Pravin Varaiya:
  Decidability of Hybrid Systems with Rectangular Differential Inclusion. 95-104
  
• Jennifer McManis, Pravin Varaiya:
  Suspension Automata: A Decidable Class of Hybrid Automata. 105-117
  
• Ahmed Bouajjani, Rachid Echahed, Riadh Robbana:
  Verification of Context-Free Timed Systems Using Linear Hybrid Observers. 118-131
  

Theory 1

• Milena Mihail, Christos H. Papadimitriou:
  On the Random Walk Method for Protocol Testing. 132-141
  
• Orna Bernholtz, Moshe Y. Vardi, Pierre Wolper:
  An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract). 142-155
  
• Anuchit Anuchitanukul, Zohar Manna:
  Realizability and Synthesis of Reactive Modules. 156-168
  
• Hardi Hungar:
  Model Checking of macro Processes. 169-181
  

Applications

• Ilan Beer, Shoham Ben-David, Daniel Geist, Raanan Gewirtzman, Michael Yoeli:
  Methodology and System for Practical Formal Verification of Reactive Hardware. 182-193
  
• Vivek G. Naik, A. Prasad Sistla:
  Modeling and Verification of a Real Life Protocol Using Symbolic Model Checking. 194-206
  
• Susanne Graf:
  Verification of a Distributed Cache Memory by Using Abstractions. 207-219
  

Invited Talk

• Zohar Manna:
  Beyond Model Checking. 220-221
  

Theory 2

• Robert P. Kurshan:
  Models Whose Checks Don't Explode. 222-233
  
• Felice Balarin, Alberto L. Sangiovanni-Vincentelli: On the Automatic Computation of Network Invariants. 234-246

Hardware Verification 1

• David Cyrluk, Paliath Narendran:
  Ground Temporal Logic: A Logic for Hardware Verification. 247-259
  
• E. Thomas Schubert:
  A Hybrid Model for Reasoning about Composed Hardware Systems. 260-272
  

Symbolic Verification 2

• Scott Hazelhurst, Carl-Johan H. Seger:
  Composing Symbolic Trajectory Evaluation Results. 273-285
  
• Zheng Zhu, Carl-Johan H. Seger:
  The Completeness of a Hardware Inference System. 286-298
  
• Daniel Geist, Ilan Beer:
  Efficient Model Checking by Automated Ordering of Transition Relation Partitions. 299-310
  
• Vigyan Singhal, Carl Pixley:
  The Verifiacation Problem for Safe Replaceability. 311-323
  

Model Checking 1

• Adnan Aziz, Thomas R. Shiple, Vigyan Singhal:
  Formula-Dependent Equivalence for Compositional CTL Model Checking. 324-337
  
• David E. Long, Anca Browne, Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero:
  An Improved Algorithm for the Evaluation of Fixpoint Expressions. 338-350
  
• Oleg Sokolsky, Scott A. Smolka:
  Incremental Model Checking in the Modal Mu-Calculus. 351-363
  

Improving Efficiency

• Bernard Cousin, Jean-Michel Hélary:
  Performance Improvement of State Space Exploration by Regular & Diffrential Hashing Functions. 364-376
  
• Doron Peled:
  Combining Partial Order Reductions with On-the-fly Model-Checking. 377-390
  
• Ramin Hojati, Robert B. Mueller-Thuns, Robert K. Brayton:
  Improving Language Containment Using Fairness Graphs. 391-403
  
• Insup Lee, Sanguthevar Rajasekaran:
  A Parallel Algorithm for Relational Coarsest Partition Problems and Its Implementation. 404-414
  

Model Checking 2

• Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi:
  Another Look at LTL Model Checking. 415-427
  
• Björn Victor, Faron Moller:
  The Mobility Workbench - A Tool for the pi-Calculus. 428-440
  

Hardware Verification 2

• Robert de Simone, Annie Ressouche:
  Compositional Semantics of ESTEREL and Verification by Compositional Reductions. 441-454
  
• Dennis Dams, Rob Gerth, Gert Döhmen, Ronald Herrmann, Peter Kelb, Hergen Pargmann:
  Model Checking Using Adaptive State and Data Abstraction. 455-467
  
• Tomas Rokicki, Chris J. Myers:
  Automatic Verification of Timed Circuits. 468-480