Presentación | Participantes | Bibliografía (DML-E) | Bibliografía adicional | Enlaces de interés | Otros proyectos DML | Ayuda  
INICIO | 28 de marzo de 2024
  

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

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.
Icono pdf Acceso al artículo completo
Equipo DML-E
Instituto de Ciencias Matemáticas (ICMAT - CSIC)
rmm()icmat.es