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.
En este artículo se resume el estado del arte de la aplicación de demostradores mecánicos de teoremas a la verificación de hardware y software comerciales. Aunque el trabajo se centra en el sistema de demostración de teoremas ACL2, que desarrollaron los autores, se citan trabajos en métodos formales muy relacionados. Este artículo tiene por objetivo satisfacer la curiosidad de aquellos lectores que se interesan por la lógica y la inteligencia artificial en lo relativo al papel que tiene la demostración mecánica de teoremas en el diseño de software y hardware hoy en día. Por otra parte, se señalan algunos de los temas claves de investigación en este campo. Estos temas van más allá de las capacidades de cualquier sistema de demostración de teoremas particular.
@article{urn:eudml:doc:41046,
title = {Some key research problems in automated theorem proving for hardware and software verification.},
journal = {RACSAM},
volume = {98},
year = {2004},
pages = {181-195},
zbl = {1103.68800},
language = {en},
url = {http://dml.mathdoc.fr/item/urn:eudml:doc:41046}
}
Kaufmann, Matt; Moore, J. Strother. Some key research problems in automated theorem proving for hardware and software verification.. RACSAM, Tome 98 (2004) pp. 181-195. http://gdmltest.u-ga.fr/item/urn:eudml:doc:41046/