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

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

Last update Tue May 21 18:54:24 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page