FORMAL METHODS IN SYSTEM DESIGN

For aims and scope, submission of papers, information and order
information see file form.inf

                        CONTENTS VOLUME 3

Volume 3, Issues 1&2, September 1993
Special Issue on Higher Order Logic Theorem Proving and its
Applications, I, edited by Luc Claesen & Michael Gordon

- Editorial by Claesen & Gordon
- The HOL Logic Extended with Quantification over Type Variables
     by Thomas F. Melham
- Lazy Techniques for Fully-Expansive Theorem Proving by Richard
     J. Boulton
- Mechanising some Advanced Refinement Concepts by J. von Wright,
     J. Hekanaho, P. Luostarinen and T. Langbacka
- Deriving Correctness Properties of Compiled Code by Paul Curzon
- A Formal Theory of Simulations Between Infinite Automata by
     Paul Loewenstein
- An Embedding of Timed Transition Systems in HOL by Roger Hale,
     Rachel Cardell-Oliver and John Herbert



                        CONTENTS VOLUME 2

Volume 2, Issue 1, February 1993

- Editorial
     Robert K. Brayton, Edmund M. Clarke, and P.A. Subrahmanyam

- Modular Abstractions for Verifying Real-Time Distributed     S  
  Systems 
     Hana De-Leon and Orna Grumberg
- On the Comparison of HOL and Boyer-Moore for Formal Hardware    
  Verification 
     C.M. Angelo, D. Verkest, L. Claesen, and H. DeMan
- Using Fixed Point Semantics to Prove Retiming Lemmas
     Stephen Brookes
- Gate-Delay-Fault Testability Properties of Multiplexor-Based    
  Networks
     Pranav Ashar, Srinivas Devadas, and Kurt Kuetzer

Volume 2, Issue 2, April 1993
Special Issue on Computer-Aided Verification: Special Methods II
Guest editor: Robert Kurshan

- Introduction
     Robert Kurshan
- A Linear-Time Model-Checking Algorithm for the Alternation-Free 
  Modal Mu-Calculus
     Rance Cleaveland and Bernhard Steffen
- Using Partial Orders for the Efficient Verification of Deadlock 
 Freedom and Safety Properties
     Patrice Godefroid and Pierre Wolper
- Structuring and Automating Hardware Proofs in a Higher-Order    
  Theorem-Proving Environment
     Ramayya Kumar, Klaus Schneider, Thomas Kropf


Volume 2, Issue 3, June 1993

- Formal Analysis of Correctness of Behavioral Transformations
     Michael C. McFarland, SJ
- A Unified Framework for Describing and Verifying Hardware       
  Synchronous Sequential Systems
     Ghislaine Thuau and Bachir Berkane
- Test Case Verification by Model Checking
     Kshirasagar Naik and Behcet Sarikaya

                        CONTENTS VOLUME 1

Volume 1, Issue 1, July 1992

- Editorial
     Robert K. Brayton, Edmund M. Clarke, and P.A. Subrahmanyam
- A Model for Synchronous Switching Circuits and its Theory of
  Correctness
     Chaochen Zhou and C.A.R. Hoare
- Specification and Automatic Verification of Self-Timed Queues
     David L. Dill, Steven M. Nowick, and Robert F. Sproull
- Probabilistic Verification of Boolean Functions
     Jawahar Jain, Jacob A. Abraham, James Bitner, and 
     Donald S. Fussell
- Asynchronous Datapaths and the Design of an Asynchronous Adder
     Alain J. Martin

Volume 1, Issues 2/3, October 1992
SPECIAL ISSUE ON COMPUTER-AIDED VERIFICATION:  GENERAL METHODS
GUEST EDITOR:  Robert Kurshan

- Introduction
     Robert Kurshan
- Formal Hardware Verification Methods:  A Survey
     Aarti Gupta
- Auto/Autograph
     Valerie Roy and Robert de Simone
- On-the-fly Verification of Finite Transition Systems
     Jean-Claude Fernandez, Laurent Mounier, Claude Jard
     and Thierry Jeron
- Memory-Efficient Algorithms for the Verification of Temporal
  Properties
     C. Courcoubetis, M. Vardi, P. Wolper and M. Yannakakis


Volume 1, Issue 4, December 1992

SPECIAL ISSUE ON COMPUTER-AIDED VERIFICATION: SPECIAL METHODS I
GUEST EDITOR: Robert Kurshan

- Introduction
     Robert Kurshan
- A Stubborn Attack on State Explosion
     Anitti Valmari
- Compositional Checking of Satisfaction
     Henrik Reif Andersen and Glynn Winskel
- Verification of a Multiprocessor Cache Protocol Using           
Simulation Relations and Higher-Order Logic
     Paul N. Loewenstein and David L. Dill
- Minimim and Maximum Delay Problems in Real-Time Systems
     Costas Courcoubetis and Mihalis Yannakakis