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 Netherlands, 22-24 June 1992
Published in June 1992
Book
Paperback/Softback
372 pages
978-0-444-89686-5 (ISBN)
Description
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.
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.
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.
More details
Series
Language
English
Place of publication
Oxford
United Kingdom
Publishing group
Elsevier Science & Technology
Target group
College/higher education
Professional and scholarly
Dimensions
Height: 230 mm
ISBN-13
978-0-444-89686-5 (9780444896865)
Copyright in bibliographic data is held by Nielsen Book Services Limited or its licensors: all rights reserved.
Schweitzer Classification
Content
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.).