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 language | English (US) |
|---|---|
| Title of host publication | Hardware Specification, Verification and Synthesis |
| Subtitle of host publication | Mathematical Aspects - Mathematical Sciences Institute Workshop, Proceedings |
| Publisher | Springer Verlag |
| Pages | 152-176 |
| Number of pages | 25 |
| Volume | 408 LNCS |
| ISBN (Print) | 9780387972268 |
| DOIs | |
| State | Published - 1990 |
| Event | Mathematical Sciences Institute Workshop on Hardware Specification, Verification and Synthesis, 1989 - Ithaca, United States Duration: Jul 5 1989 → Jul 7 1989 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 408 LNCS |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Other
| Other | Mathematical Sciences Institute Workshop on Hardware Specification, Verification and Synthesis, 1989 |
|---|---|
| Country | United States |
| City | Ithaca |
| Period | 7/5/89 → 7/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