7. CAV 1995: Liège, Belgium

Session 1: Invited Talk

• Randal E. Bryant:
  Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract). 1-3
  

Session 2

• Jochen Bern, Christoph Meinel, Anna Slobodová:
  Global rebuilding of OBDDs Avoiding Memory Requirement Maxima. 4-15
  
• Ashvin Dsouza, Bard Bloom:
  Generating BDD Models for Process Algebra Terms. 16-30
  
• David A. Basin, Nils Klarlund:
  Hardware Verification using Monadic Second-Order Logic. 31-41
  
• Bengt Jonsson, Lars Kempe:
  Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms. 42-53
  

Session 3

• Jürgen Dingel, Thomas Filkorn:
  Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving. 54-69
  
• E. Pascal Gribomont, Didier Rossetto:
  CAVEAT: Technique and Tool for Computer Aided VErification And Transformation. 70-83
  
• S. Rajan, Natarajan Shankar, Mandayam K. Srivas:
  An Integration of Model Checking with Automated Proof Checking. 84-97
  

Session 4

• Ramin Hojati, Robert K. Brayton:
  Automatic Datapath Abstraction In Hardware Systems. 98-113
  
• Antoine Rauzy:
  Toupie = µ-Calculus + Constraints. 114-126
  
• Lalita Jategaonkar Jagadeesan, Carlos Puchol, James Von Olnhausen:
  Safety Property Verification of ESTEREL Programs and Applications to Telecommunications Software. 127-140
  

Session 5: Invited Tutorial

• E. Allen Emerson:
  Methods for Mu-calculus Model Checking: A Tutorial (Abstract). 141
  

Session 6

• Henrik Reif Andersen, Bart Vergauwen:
  Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion. 142-154
  
• Adnan Aziz, Vigyan Singhal, Felice Balarin:
  It Usually Works: The Temporal Logic of Stochastic Systems. 155-165
  
• Rajeev Alur, Thomas A. Henzinger:
  Local Liveness for Compositional Modeling of Fair Reactive Systems. 166-179
  
• Kenneth L. McMillan:
  Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. 180-195
  

Session 7

• Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana:
  From Duration Calculus To Linear Hybrid Automata. 196-210
  
• Oleg Sokolsky, Scott A. Smolka:
  Local Model Checking for Real-Time Systems (Extended Abstract). 211-224
  
• Thomas A. Henzinger, Pei-Hsin Ho:
  Algorithmic Analysis of Nonlinear Hybrid Systems. 225-238
  

Session 8

• Helmut Lescow:
  On Polynomial-Size Programs Winning Finite-State Games. 239-252
  
• Sriram C. Krishnan, Anuj Puri, Robert K. Brayton, Pravin Varaiya:
  The Rabin Index and Chain Automata, with Applications to Automatas and Games. 253-266
  
• Moshe Y. Vardi:
  An Automata-Theoretic Approach to Fair Realizability and Synthesis. 267-278
  
• Adnan Aziz, Felice Balarin, Robert K. Brayton, M. D. DiBenedetto, Alexander Saldanha:
  Supervisory Control of Finite State Machines. 279-292
  

Session 9: Invited Talk

• Patrick Cousot, Radhia Cousot:
  Compositional and Inductive Semantic Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form. 293-308
  

Session 10

• E. Allen Emerson, A. Prasad Sistla:
  Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach. 309-324
  
• Orna Kupferman:
  Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions. 325-338
  
• Robert P. Kurshan, Michael Merritt, Ariel Orda, Sonia R. Sachs:
  Modelling Asynchrony with a Synchronous Model. 339-352
  
• Javier Esparza, Astrid Kiehn:
  On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes. 353-366
  

Sesion 11

• Ásgeir Th. Eiríksson, Kenneth L. McMillan:
  Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study. 367-380
  
• Pei-Hsin Ho, Howard Wong-Toi:
  Automated Analysis of an Audio Control Protocol. 381-394
  
• Colin J. Fidge, Peter Kearney, Mark Utting:
  Interactively Verifying a Simple Real-time Scheduler. 395-408
  

Session 12

• David L. Dill, Howard Wong-Toi:
  Verification of Real-Time Systems by Successive Over and Under Approximation. 409-422
  
• Henrik Hulgaard, Steven M. Burns:
  Efficient Timing Analysis of a Class of Petri Nets. 423-436
  
• Ahmed Bouajjani, Riadh Robbana:
  Verifying omega-Regular Properties for a Subclass of Linear Hybrid Systems. 437-450