Implementing and verifying finite-state machines using types in higher-order logic

Shiu Kai Chin, Graham Birtwistle

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

The combination of declarative functional languages, formal logic, and mechanical theorem-pro vers offers the opportunity to extend current CAD tools dealing with finite-state machine synthesis and verification. Theorems are proved showing equivalence between machines under certain correctness conditions. Implementations are related to one another and to specifications where the state, input, and output alphabets are viewed as data types.

Original languageEnglish (US)
Title of host publicationProceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications
EditorsMyla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages121-129
Number of pages9
ISBN (Electronic)0818624604, 9780818624605
DOIs
StatePublished - Jan 1 1991
Event1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications - Davis, United States
Duration: Aug 28 1991Aug 30 1991

Publication series

NameProceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications

Conference

Conference1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications
CountryUnited States
CityDavis
Period8/28/918/30/91

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Logic
  • Computer Science Applications
  • Hardware and Architecture
  • Software
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Implementing and verifying finite-state machines using types in higher-order logic'. Together they form a unique fingerprint.

  • Cite this

    Chin, S. K., & Birtwistle, G. (1991). Implementing and verifying finite-state machines using types in higher-order logic. In M. Archer, J. J. Joyce, K. N. Levitt, & P. J. Windley (Eds.), Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications (pp. 121-129). [596279] (Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/HOL.1991.596279