5. CAV 1993: Elounda, Greece

Invited Lecture

• Robert K. Brayton:
  Logic Synthesis and Design Verification. 1-2
  

Session 1: hardware Verification with BDDs

• Alan J. Hu, David L. Dill:
  Efficient Verification with BDDs using Implicitly Conjoined Invariants. 3-14
  
• Aarti Gupta, Allan L. Fisher:
  Parametric Circuit Representation Using Inductive Boolean Functions. 15-28
  
• Felice Balarin, Alberto L. Sangiovanni-Vincentelli:
  An Iterative Approach to Language Containment. 29-40
  
• Ramin Hojati, Robert K. Brayton, Robert P. Kurshan:
  BDD-Based Debugging Of Design Using Language Containment and Fair CTL. 41-58
  

Session 2: Methods and Tools

• Pierre Wolper, Denis Leroy:
  Reliable Hashing without Collosion Detection. 59-70
  
• Susanne Graf, Claire Loiseaux:
  A Tool for Symbolic Program Verification and Abstration. 71-84
  
• Jean-Claude Fernandez, Alain Kerbrat, Laurent Mounier:
  Symbolic Equivalence Checking. 85-96
  
• Yonit Kesten, Zohar Manna, Hugh McGuire, Amir Pnueli:
  A Decision Algorithm for Full Propositional Temporal Logic. 97-109
  
• A. S. Krishnakumar:
  Reachability and Recurrence in Extended Finite State Machines: Modular Vector Addition Systems. 110-122
  
• June-Kyung Rho, Fabio Somenzi:
  Automatic Generation of Network Invariants for the Verification of Iterative Sequential Systems. 123-137
  
• G. Kutty, Y. S. Ramakrishna, Louise E. Moser, Laura K. Dillon, P. M. Melliar-Smith:
  A Graphical Interval Logic Toolset for Verifying Concurrent Systems. 138-153
  

Session 3: Theorem Proving 1

• Hardi Hungar:
  Combining Model Checking and Theorem Proving to Verify Parallel Processes. 154-165
  
• Robert P. Kurshan, Leslie Lamport:
  Verification of a Multiplier: 64 Bits and Beyond. 166-179
  
• Pravin Varaiya:
  Protocol Design for an Automated Highway System (Abstract). 180
  

Session 4: Analysis of Real-Time Systems 1

• Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger:
  Computing Accumulated Delays in Real-time Systems. 181-193
  
• Oded Maler, Amir Pnueli:
  Reachability Analysis of Planar Multi-limear Systems. 194-209
  
• Mihalis Yannakakis, David Lee:
  An Efficient Algorithm for Minimizing Real-time Transition Systems. 210-224
  
• Costas Courcoubetis, Werner Damm, Bernhard Josko:
  Verification of timing Properties of VHDL. 225-236
  
• William K. C. Lam, Robert K. Brayton:
  Alternating RQ Timed Automata. 237-252
  
• Karlis Cerans, Jens Chr. Godskesen, Kim Guldstrand Larsen:
  Timed Modal Specification - Theory and Tools. 253-267
  

Session 5: Theorem Proving 2

• Matthew Wilding:
  A Mechanically Verified Application for a Mechanically Verified Environment. 268-279
  
• Natarajan Shankar:
  Verification of Real-Time Systems Using PVS. 280-291
  
• Patrick Lincoln, John M. Rushby:
  The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model. 292-304
  
• Jørgen F. Søgaard-Andersen, Stephen J. Garland, John V. Guttag, Nancy A. Lynch, Anna Pogosyants:
  Computer-Assisted Simulation Proofs. 305-319
  

Invited Lecture

• Michael J. C. Gordon:
  A Verifier and Timing Analyser for Simple Imperative Programs (Abstract). 320
  

Session 6: Analysis of Real-Time Systems 2

• Tomohiro Yoneda, Atsufumi Shibayama, Bernd-Holger Schlingloff, Edmund M. Clarke:
  Efficient Verification of Parallel Real-Time Systems. 321-346
  
• Nicolas Halbwachs:
  Delay Analysis in Synchronous Programs. 333-346
  
• Martin Jourdan, Florence Maraninchi, Alfredo Olivero:
  Verifying Quantitative Real-Time Properties of Synchronous Programs. 347-358
  
• Matthew Hennessy, Xinxin Liu:
  A Modal Logic for Message passing Processes (Extended Abstract). 359-370
  
• Ed Brinksma, Rom Langerak, Peter Broekroelofs:
  Functionality Decomposition by Compositional Correstness Preserving Transformation. 371-384
  
• E. Allen Emerson, Charanjit S. Jutla, A. Prasad Sistla:
  On Model-Checking for Fragments of µ-Calculus. 385-396
  

Session 8: Partial Orders

• Antti Valmari:
  On-the-Fly Verification with Stubborn Sets. 397-408
  
• Doron Peled:
  All from One, One for All: on Model Checking Using Representatives. 409-423
  
• David K. Probst, Hon Fung Li:
  Verifying Timed Behavior Automata with Input/Output Critical Races. 424-437
  
• Patrice Godefroid, Didier Pirottin:
  Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract). 438-449
  

Session 9: Exploiting Symmetry

• Edmund M. Clarke, Thomas Filkorn, Somesh Jha:
  Exploiting Symmetry In Temporal Logic Model Checking. 450-462
  
• E. Allen Emerson, A. Prasad Sistla:
  Symmetry and Model Checking. 463-478
  
• Dennis Dams, Orna Grumberg, Rob Gerth:
  Generation of Reduced Models for Checking Fragments of CTL. 479-490
  
• Robert P. Kurshan, Michael Merritt, Ariel Orda, Sonia R. Sachs:
  A Structural Linearization Principle for Processes. 491-504
  

Last update Sat May 18 18:12:30 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page