Theorem provers in circuit design : proceedings of the IFIP TC10/WG10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice, and Experience, Nijmegen, the Netherlands, 22-24 June 1992
Author(s)
Bibliographic Information
Theorem provers in circuit design : proceedings of the IFIP TC10/WG10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice, and Experience, Nijmegen, the Netherlands, 22-24 June 1992
(IFIP transactions, A . Computer science and technology ; 10)
North-Holland, 1992
Available at 8 libraries
  Aomori
  Iwate
  Miyagi
  Akita
  Yamagata
  Fukushima
  Ibaraki
  Tochigi
  Gunma
  Saitama
  Chiba
  Tokyo
  Kanagawa
  Niigata
  Toyama
  Ishikawa
  Fukui
  Yamanashi
  Nagano
  Gifu
  Shizuoka
  Aichi
  Mie
  Shiga
  Kyoto
  Osaka
  Hyogo
  Nara
  Wakayama
  Tottori
  Shimane
  Okayama
  Hiroshima
  Yamaguchi
  Tokushima
  Kagawa
  Ehime
  Kochi
  Fukuoka
  Saga
  Nagasaki
  Kumamoto
  Oita
  Miyazaki
  Kagoshima
  Okinawa
  Korea
  China
  Thailand
  United Kingdom
  Germany
  Switzerland
  France
  Belgium
  Netherlands
  Sweden
  Norway
  United States of America
Description and Table of Contents
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.
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.).
by "Nielsen BookData"