Ponencia
Formal Reasoning about Efficient Data Structures: A Case Study in ACL2
Autor/es | Ruiz Reina, José Luis
Alonso Jiménez, José Antonio Hidalgo Doblado, María José Martín Mateos, Francisco Jesús |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2003 |
Fecha de depósito | 2019-05-09 |
Publicado en |
|
ISBN/ISSN | 978-3-540-22174-6 0302-9743 |
Resumen | We describe in this paper the formal verification, using the
ACL2 system, of a syntactic unification algorithm where terms are represented
as directed acyclic graphs (dags) and these graphs are stored
in a single-threaded ... We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms are represented as directed acyclic graphs (dags) and these graphs are stored in a single-threaded object (stobj). The use of stobjs allows destructive operations on data (thus improving the performance of the algorithm), while maintaining the applicative semantics of ACL2. We intend to show how ACL2 provides an environment where execution of algorithms with efficient data structures and formal reasoning about them can be carried out. |
Identificador del proyecto | TIC2000-1368-C03-02 |
Cita | Ruiz Reina, J.L., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Martín Mateos, F.J. (2003). Formal Reasoning about Efficient Data Structures: A Case Study in ACL2. En LOPSTR 2003: 13th International Symposium on Logic-Based Program Synthesis and Transformation (75-91), Uppsala, Sweden: Springer. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
Formal Reasoning about Efficient ... | 409.2Kb | [PDF] | Ver/ | |