Ponencia
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
Autor/es | Martín Mateos, Francisco Jesús
Rubio, Julio Ruiz Reina, José Luis |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2009 |
Fecha de depósito | 2019-05-03 |
Publicado en |
|
ISBN/ISSN | 978-3-642-02613-3 0302-9743 |
Resumen | Kenzo is a Computer Algebra system devoted to Algebraic
Topology, and written in the Common Lisp programming language. It is
a descendant of a previous system called EAT (for Effective Algebraic
Topology). Kenzo shows ... Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It is a descendant of a previous system called EAT (for Effective Algebraic Topology). Kenzo shows a much better performance than EAT due, among other reasons, to a smart encoding of degeneracy lists as integers. In this paper, we give a complete automated proof of the correctness of this encoding used in Kenzo. The proof is carried out using ACL2, a system for proving properties of programs written in (a subset of) Common Lisp. The most interesting idea, from a methodological point of view, is our use of EAT to build a model on which the verification is carried out. Thus, EAT, which is logically simpler but less efficient than Kenzo, acts as a mathematical model and then Kenzo is formally verified against it. |
Identificador del proyecto | MTM2006-06513 |
Cita | Martín Mateos, F.J., Rubio, J. y Ruiz Reina, J.L. (2009). ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. En CICM 2009: International Conference on Intelligent Computer Mathematics (106-121), Grand Bend, Canada: Springer. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
ACL2 Verification of Simplicial ... | 292.5Kb | [PDF] | Ver/ | |