Computer-aided verification
The work
| Authors | E. M. Clarke; Robert P. Kurshan |
|---|---|
| Editors | |
| Type | article |
| Year | 1996 |
| Citekey | clarke1996computeraided |
Where it appeared
| Published in | IEEE Spectrum |
|---|---|
| Publisher | Institute of Electrical and Electronics Engineers |
| Volume | 33 |
| Issue | 6 |
| Pages | 61--67 |
Identifiers
| DOI | 10.1109/6.499951 |
|---|---|
| OpenAlex | W4244847755 |
Access
| Landing page | https://doi.org/10.1109/6.499951 |
|---|
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
Theorem proving and model checking are powerful tools that can verify the logical correctness of today's ICs or find their hidden bugs. Today, the first computer-aided verification tools are becoming commercially available. They are based on methods that in many cases can reduce the complexity of verification (without sacrificing guaranteed correctness) to such a degree that it becomes computationally feasible. Among the most powerful of these methods are symbolic model-checking and homomorphic reduction, both of which represent a complex system in terms of a compact and computationally more tractable structure. Moreover, the two can be used together with a multiplicative reduction effect, since they work independently of one another. Of special importance is the fact that they each can be implemented automatically, so the task of reduction is programmed into the computer rather than presenting a burden to the design engineer.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-23 21:14 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{clarke1996computeraided,
title = {Computer-aided verification},
author = {E. M. Clarke and Robert P. Kurshan},
year = {1996},
journal = {IEEE Spectrum},
publisher = {Institute of Electrical and Electronics Engineers},
volume = {33},
number = {6},
pages = {61--67},
doi = {10.1109/6.499951},
}
This record lives at https://refs.drheap.org/clarke1996computeraided/ and will keep doing so.