Verifying a logic-synthesis algorithm and implementation: a case study in software verification
The work
| Authors | Mark D. Aagaard; Miriam E. Leeser |
|---|---|
| Editors | |
| Type | article |
| Year | 1995 |
| Citekey | aagaard1995verifying |
Where it appeared
| Published in | IEEE Transactions on Software Engineering |
|---|---|
| Publisher | IEEE Computer Society |
| Volume | 21 |
| Issue | 10 |
| Pages | 822--833 |
Identifiers
| DOI | 10.1109/32.469458 |
|---|---|
| OpenAlex | W2113856522 |
Access
| Landing page | https://doi.org/10.1109/32.469458 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
We describe the verification of a logic synthesis tool with the Nuprl proof development system. The logic synthesis tool, Pbs, implements the weak division algorithm. Pbs consists of approximately 1000 lines of code implemented in a functional subset of Standard ML. It is a proven and usable implementation and is an integral part of the Bedroc high level synthesis system. The program was verified by embedding the subset of Standard ML in Nuprl and then verifying the correctness of the implementation of Pbs in the Nuprl logic. The proof required approximately 500 theorems. In the process of verifying Pbs we developed a consistent approach for using a proof development system to reason about functional programs. The approach hides implementation details and uses higher order theorems to structure proofs and aid in abstract reasoning. Our approach is quite general, should be applicable to any higher order proof system, and can aid in the future verification of large software implementations.>
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 10:43 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{aagaard1995verifying,
title = {Verifying a logic-synthesis algorithm and implementation: a case study in software verification},
author = {Mark D. Aagaard and Miriam E. Leeser},
year = {1995},
journal = {IEEE Transactions on Software Engineering},
publisher = {IEEE Computer Society},
volume = {21},
number = {10},
pages = {822--833},
doi = {10.1109/32.469458},
}
This record lives at https://refs.drheap.org/aagaard1995verifying/ and will keep doing so.