Combining engineering vigor with mathematical rigor

Shiu Kai Chin

doi:10.1007/0-387-97226-9_28

Combining engineering vigor with mathematical rigor

Shiu Kai Chin

Department of Electrical Engineering & Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Hardware Specification, Verification and Synthesis
Subtitle of host publication	Mathematical Aspects - Mathematical Sciences Institute Workshop, Proceedings
Editors	Miriam Leeser, Geoffrey Brown
Publisher	Springer Verlag
Pages	152-176
Number of pages	25
ISBN (Print)	9780387972268
DOIs	https://doi.org/10.1007/0-387-97226-9_28
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)

Access to Document

10.1007/0-387-97226-9_28

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 M. Leeser, & G. Brown (Eds.), Hardware Specification, Verification and Synthesis: Mathematical Aspects - Mathematical Sciences Institute Workshop, Proceedings (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

Combining engineering vigor with mathematical rigor. / Chin, Shiu Kai.

Hardware Specification, Verification and Synthesis: Mathematical Aspects - Mathematical Sciences Institute Workshop, Proceedings. ed. / Miriam Leeser; Geoffrey Brown. Springer Verlag, 1990. p. 152-176 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 408 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Chin, SK 1990, Combining engineering vigor with mathematical rigor. in M Leeser & G Brown (eds), Hardware Specification, Verification and Synthesis: Mathematical Aspects - Mathematical Sciences Institute Workshop, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 408 LNCS, Springer Verlag, pp. 152-176, Mathematical Sciences Institute Workshop on Hardware Specification, Verification and Synthesis, 1989, Ithaca, United States, 7/5/89. https://doi.org/10.1007/0-387-97226-9_28

Chin SK. Combining engineering vigor with mathematical rigor. In Leeser M, Brown G, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects - Mathematical Sciences Institute Workshop, Proceedings. Springer Verlag. 1990. p. 152-176. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/0-387-97226-9_28

Chin, Shiu Kai. / Combining engineering vigor with mathematical rigor. Hardware Specification, Verification and Synthesis: Mathematical Aspects - Mathematical Sciences Institute Workshop, Proceedings. editor / Miriam Leeser ; Geoffrey Brown. Springer Verlag, 1990. pp. 152-176 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{56ab923e05f8454cafb9c12e40e81e1a,

title = "Combining engineering vigor with mathematical rigor",

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.",

author = "Chin, {Shiu Kai}",

note = "Funding Information: §This work was partially supported by NSF Grant MIP-8710826, IBM Contract 845, and Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1990. Copyright: Copyright 2017 Elsevier B.V., All rights reserved.; Mathematical Sciences Institute Workshop on Hardware Specification, Verification and Synthesis, 1989 ; Conference date: 05-07-1989 Through 07-07-1989",

year = "1990",

doi = "10.1007/0-387-97226-9_28",

language = "English (US)",

isbn = "9780387972268",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "152--176",

editor = "Miriam Leeser and Geoffrey Brown",

booktitle = "Hardware Specification, Verification and Synthesis",

}

TY - GEN

T1 - Combining engineering vigor with mathematical rigor

AU - Chin, Shiu Kai

N1 - Funding Information: §This work was partially supported by NSF Grant MIP-8710826, IBM Contract 845, and Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1990. Copyright: Copyright 2017 Elsevier B.V., All rights reserved.

PY - 1990

Y1 - 1990

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85032211923&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85032211923&partnerID=8YFLogxK

U2 - 10.1007/0-387-97226-9_28

DO - 10.1007/0-387-97226-9_28

M3 - Conference contribution

AN - SCOPUS:85032211923

SN - 9780387972268

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 152

EP - 176

BT - Hardware Specification, Verification and Synthesis

A2 - Leeser, Miriam

A2 - Brown, Geoffrey

PB - Springer Verlag

T2 - Mathematical Sciences Institute Workshop on Hardware Specification, Verification and Synthesis, 1989

Y2 - 5 July 1989 through 7 July 1989

ER -