Name
Abstract | ||
|---|---|---|
The promise of cost savings and guaranteed product reliability that have been claimed for formal verification of digital hardware have yet to be realised in practice. Largely, this is because it can be extraordinarily difficult and tedious verifying even a simple design. A large part of this difficulty is caused by the absence of much of real-world engineering theory in available theorem provers. The paper describes the formalisation of deterministic and non-deterministic state-machine theory in the HOL theorem prover. Proofs using the theory are not only shorter, but are much more tractable, and follow standard engineering reasoning much more closely than direct proofs without using the theory. |
Year | DOI | Venue |
|---|---|---|
1989 | 10.1007/0-387-97226-9_24 | Proceedings of the Mathematical Sciences Institute workshop on Hardware specification, verification and synthesis: mathematical aspects |
Keywords | Field | DocType |
state machine,higher-order logic,state machines,theorem prover,higher order logic,formal verification | HOL,Automated reasoning,Automated theorem proving,Finite-state machine,Theoretical computer science,First-order logic,Mathematical proof,Higher-order logic,Mathematics,Formal verification | Conference |
Volume | ISSN | ISBN |
408 | 0302-9743 | 0-387-97226-9 |
Citations | PageRank | References |
6 | 3.08 | 5 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Paul Loewenstein | 1 | 6 | 3.08 |