@inproceedings{4b2af56798374ce3874efe5e47c926cd,

title = "Verifying arithmetic hardware in higher-order logic",

abstract = "Theorem-based design uses logical inference rather than simulation to determine or verify the properties of design implementations. The initial effort to make such an approach practical is large when compared to conventional simulation. However, the cost of this effort is typically incurred only once. The hardware descriptions are parameterized so that the verification results are applicable to an entire set of designs rather than just one instantiation. To illustrate these ideas, the logical structure used to verify arithmetic hardware in HOL is outlined. In particular, the role of data abstraction, r0ecursion, and induction is shown.",

author = "Chin, {Shiu Kai}",

note = "Publisher Copyright: {\textcopyright} 1991 Institute of Electrical and Electronics Engineers Inc. All rights reserved.; 1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications ; Conference date: 28-08-1991 Through 30-08-1991",

year = "1991",

doi = "10.1109/HOL.1991.596268",

language = "English (US)",

series = "Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "22--31",

editor = "Myla Archer and Joyce, {Jeffrey J.} and Levitt, {Karl N.} and Windley, {Phillip J.}",

booktitle = "Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications",

}