Formal Methods in System Design, Volume 3

Volume 3, Number 1/2, 1993

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

Volume 3, Number 3, 1993

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