Título inglés |
Some key research problems in automated theorem proving for hardware and software verification. |
Título español |
Algunos problemas claves de investigación en la demostración mecánica de teoremas para la verificación de hardware y software. |
Autor/es |
Kaufmann, Matt ; Moore, J. Strother |
Organización |
Adv. Micro Devic. Inc., Austin (Texas), Estados Unidos;Dep. Comput. Sci. Univ. Texas Austin, Austin (Texas), Estados Unidos |
Revista |
1578-7303 |
Publicación |
2004, 98 (1): 181-195, 44 Ref. |
Tipo de documento |
articulo |
Idioma |
Inglés |
Resumen español |
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. |
Resumen inglés |
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. |
Acceso al artículo completo |