Combining engineering vigor with mathematical rigor

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

Abstract

Higher order logic and a functional language are used to document and verify design procedures which correctly synthesize array multipliers of arbitrary size. The procedures work with general negabinary inputs and create design descriptions corresponding to practical designs which are correct-by-construction.

Original languageEnglish (US)
Title of host publicationHardware Specification, Verification and Synthesis
Subtitle of host publicationMathematical Aspects - Mathematical Sciences Institute Workshop, Proceedings
PublisherSpringer Verlag
Pages152-176
Number of pages25
Volume408 LNCS
ISBN (Print)9780387972268
DOIs
StatePublished - 1990
EventMathematical Sciences Institute Workshop on Hardware Specification, Verification and Synthesis, 1989 - Ithaca, United States
Duration: Jul 5 1989Jul 7 1989

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume408 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherMathematical Sciences Institute Workshop on Hardware Specification, Verification and Synthesis, 1989
CountryUnited States
CityIthaca
Period7/5/897/7/89

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Combining engineering vigor with mathematical rigor'. Together they form a unique fingerprint.

  • Cite this

    Chin, S. K. (1990). Combining engineering vigor with mathematical rigor. In Hardware Specification, Verification and Synthesis: Mathematical Aspects - Mathematical Sciences Institute Workshop, Proceedings (Vol. 408 LNCS, pp. 152-176). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 408 LNCS). Springer Verlag. https://doi.org/10.1007/0-387-97226-9_28