Theorem Provers in Circuit Design: Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, Nijmegen, The (IFIP Transactions A: Computer Science and Technology)

The papers in this volume address the role of mechanized theorem proving technology in the design of digital systems. The primary focus is on the practical application of theorem provers to digital design, rather than on theoretical foundations. The diverse contributions include invited papers by the leading researchers Gordon and Hunt as well as technical contributions by many other prominent researchers in the field of machine-assisted hardware verification. This side of the Proceedings reflects current research activity and the section containing tutorial papers on several influential theorem provers serves as an introduction to this exciting field.

Table of Contents:
Research Papers. Invited paper: Introduction to a Formally Defined Hardware Description Language (B.C. Brock, W.A. Hunt, Jr. and W.D. Young). A Description Methodology for Parameterized Modules in the Boyer-Moore Logic (D. Verkest et al.) Hierarchical Mixed-mode Verification of Complex FSMs Described at the RT Level (T. Margaria). Implementation of the Veritas Design Logic (K. Hanna, N. Daeche and G. Howells). Synchronous Realization of Asynchronous Computations (H.H. Lovengreen and J. Staunstrup). Modelling and Verification of Timing Conditions with the Boyer Moore Prover (D.J. Kinniment and A.M. Koelmans). Invited paper: Experience with Embedding Hardware Description Languages in HOL (R. Boulton et al.). Incremental Design and Formal Verification of Microcoded Microprocessors (J.M.J. Herbert). Transformational Design in a Theorem Prover (H. Busch). FUNNEL and 2OBJ: Towards an Integrated Hardware Design Environment (V. Stavridou et al.). Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based Verification (M. Bickford and M. Srivas). Theorem Proving as an Industrial Tool for System Level Design (S. Bainbridge, A. Camilleri and R. Fleming). Tutorial Papers. Mechanized Verification of Circuit Descriptions Using the Larch Prover (J. Staunstrup, S.J. Garland and J.V. Guttag). The Veritas Design Logic: A User's View (K. Hanna and N. Daeche). Nuprl and its Use in Circuit Design (P.B. Jackson). Using the State Delta Verification System (SDVS) for Hardware Verification (B. Levy et al.).