ACL2 verification of simplicial degeneracy programs in the Kenzo system
- Martín-Mateos, F.-J. 1
- Rubio, J. 2
- Ruiz-Reina, J.-L. 1
-
1
Universidad de Sevilla
info
-
2
Universidad de La Rioja
info
Editorial: SPRINGER-VERLAG
ISBN: 978-3-642-02614-0
Año de publicación: 2009
Volumen: 5625 LNAI
Páginas: 106-121
Tipo: Capítulo de Libro
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 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. © 2009 Springer-Verlag Berlin Heidelberg.