Abstract is missing.
- Introduction to a Formally Defined Hardware Description LanguageBishop Brock, Warren A. Hunt Jr., William D. Young. 3-35
- A Description Methodology for Parameterized Modules in the Boyer-Moore LogicDiederik Verkest, J. Vandenbergh, Luc J. M. Claesen, Hugo De Man. 37-57
- Hierarchical Mixed-Mode Verification of Complex FSMs Described at the RT LevelTiziana Margaria. 59-75
- Implementation of the Veritas Design LogicKeith Hanna, Neil Daeche, Gareth Howells. 77-94
- Synchronous Realization of Asynchronous ComputationsHans Henrik Løvengreen, Jørgen Staunstrup. 95-110
- Modelling and Verification of Timing Conditions with the Boyer Moore ProverD. J. Kinniment, Albert Koelmans. 111-127
- Experience with Embedding Hardware Description Languages in HOLRichard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel. 129-156
- Incremental Design and Formal Verification of Microcoded MicroporcessorsJohn Herbert. 157-174
- Transformational Design in a Theorem ProverHolger Busch. 175-196
- FUNNEL and 2OBJ: Towards an Integrated Hardware Design EnvironmentVictoria Stavridou, Joseph A. Goguen, A. Stevens, S. M. Eker, S. N. Aloneftis, K. M. Hobley. 197-223
- Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based VerificationMark Bickford, Mandayam K. Srivas. 225-251
- Theorem Proving as an Industrial Tool for System Level DesginSimon Bainbridge, Albert John Camilleri, Roger Fleming. 253-274
- Mechanized Verification of Circuit Descriptions Using the Larch ProverJørgen Staunstrup, Stephen J. Garland, John V. Guttag. 277-299
- The Veritas Design Logic: A User s ViewKeith Hanna, Neil Daeche. 301-310
- Nuprl and Its Use in Circuit DesignPaul B. Jackson. 311-336
- Using the State Delta Verification System (SDVS) for Hardware VerificationBeth Levy, Ivan Filippenko, Leo Marcus, Telis Menas. 337-360