Some key research problems in automated theorem proving for hardware and software verification.

Kaufmann, Matt, and Moore, J. Strother. "Some key research problems in automated theorem proving for hardware and software verification.." RACSAM 98.1 (2004): 181-195. <http://eudml.org/doc/41046>.

@article{Kaufmann2004,
abstract = {This paper sketches the state of the art in the application of mechanical theorem provers to the verification of commercial computer hardware and software. While the paper focuses on the theorem proving system ACL2, developed by the two authors, it references much related work in formal methods. The paper is intended to satisfy the curiosity of readers interested in logic and artificial intelligence as to the role of mechanized theorem proving in hardware and software design today. In addition, it points out some of the key research topics in the area. These topics transcend any one particular theorem proving system.},
author = {Kaufmann, Matt, Moore, J. Strother},
journal = {RACSAM},
language = {eng},
number = {1},
pages = {181-195},
title = {Some key research problems in automated theorem proving for hardware and software verification.},
url = {http://eudml.org/doc/41046},
volume = {98},
year = {2004},
}

TY - JOUR
AU - Kaufmann, Matt
AU - Moore, J. Strother
TI - Some key research problems in automated theorem proving for hardware and software verification.
JO - RACSAM
PY - 2004
VL - 98
IS - 1
SP - 181
EP - 195
AB - This paper sketches the state of the art in the application of mechanical theorem provers to the verification of commercial computer hardware and software. While the paper focuses on the theorem proving system ACL2, developed by the two authors, it references much related work in formal methods. The paper is intended to satisfy the curiosity of readers interested in logic and artificial intelligence as to the role of mechanized theorem proving in hardware and software design today. In addition, it points out some of the key research topics in the area. These topics transcend any one particular theorem proving system.
LA - eng
UR - http://eudml.org/doc/41046
ER -