Formal Methods in System Design, Volume 3

Volume 3, Number 1/2, 1993

Special Issue on Higher Order Logic Theorem Proving and its Applications I

• 
  Thomas F. Melham:
  The HOL Logic Extended with Quantification over Type Variables. 7-24
• 
  Richard J. Boulton:
  Lazy Techniques for Fully Expansive Theorem Proving. 25-47
• 
  Joakim von Wright, Jukka Hekanaho, P. Luostarinen, Thomas Långbacka:
  Mechanizing Some Advanced Refinement Concepts. 49-81
• 
  Paul Curzon:
  Deriving Correctness Properties of Compiled Code. 83-115
• 
  Paul Loewenstein:
  A Formal Theory of Simulations between Infinite Automata. 117-149
• 
  Roger Hale, Rachel Cardell-Oliver, John Herbert:
  An Embedding of Timed Transition Systems in HOL. 151-174

Volume 3, Number 3, 1993

Special Issue on Designing Correct Circuits

• 
  James B. Saxe, James J. Horning, John V. Guttag, Stephen J. Garland:
  Using Transformations and Verification in Circuit Design. 181-209
• 
  Jo C. Ebergen, Ad M. G. Peeters:
  Design and Analysis of Delay-Insensitive Modulo-N Counters. 211-232
• 
  Michael Mendler, Terry Stroup:
  Newtonian Arbiters Cannot be Proven Correct. 233-257