Artículo
A verified Common Lisp implementation of Buchberger's algorithm in ACL2
Autor/es | Medina Bulo, Inmaculada
Palomo Lozano, Francisco Ruiz Reina, José Luis |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2010 |
Fecha de depósito | 2019-05-03 |
Publicado en |
|
Resumen | In this article, we present the formal verification of a Common
Lisp implementation of Buchberger's algorithm for computing
Gröbner bases of polynomial ideals. This work is carried out in
ACL2, a system which provides ... In this article, we present the formal verification of a Common Lisp implementation of Buchberger's algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort. |
Cita | Medina Bulo, I., Palomo Lozano, F. y Ruiz Reina, J.L. (2010). A verified Common Lisp implementation of Buchberger's algorithm in ACL2. Journal of Symbolic Computation, 45 (1), 96-123. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
A verified Common Lisp impleme ... | 434.3Kb | [PDF] | Ver/ | |