Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleA verified Common Lisp implementation of Buchberger’s algorithm in ACL2
Author(s) Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José-Luis Ruiz-Reina
TypeArticle in Journal
AbstractIn 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.
URL http://www.sciencedirect.com/science/article/pii/S0747717109001357
JournalJournal of Symbolic Computation
Pages96 - 123
Translation No
Refereed No