Correct Safety Critical Hardware Descriptions via Static Analysis and Theorem Proving
The work
| Authors | Nicholas Moore; Mark S. Lawford |
|---|---|
| Editors | |
| Type | misc |
| Year | 2017 |
| Citekey | moore2017correct |
Where it appeared
| Volume | 7041 |
|---|---|
| Pages | 58--64 |
Identifiers
| DOI | 10.1109/formalise.2017.11 |
|---|---|
| OpenAlex | W4233622121 |
Access
| Landing page | https://doi.org/10.1109/formalise.2017.11 |
|---|
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 propose a new method for embedding Bluespec SystemVerilog descriptions in PVS's higher-order proof logic. In contrast to previous embeddings, our approach accepts a greater subset of BSV and provides a far greater degree of automation. Our custom software tool transforms the action-oriented semantics of BSV to a state-centric Kripke structure, enabling automated theorem proving. We demonstrate our verification technique by applying it to one of the function blocks of the IEC 61131-3 standard for PLCs.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 17:23 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@misc{moore2017correct,
title = {Correct Safety Critical Hardware Descriptions via Static Analysis and Theorem Proving},
author = {Nicholas Moore and Mark S. Lawford},
year = {2017},
volume = {7041},
pages = {58--64},
doi = {10.1109/formalise.2017.11},
}
This record lives at https://refs.drheap.org/moore2017correct/ and will keep doing so.