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

Details:

   
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.
ISSN0747-7171
URL http://www.sciencedirect.com/science/article/pii/S0747717109001357
LanguageEnglish
JournalJournal of Symbolic Computation
Volume45
Number1
Pages96 - 123
Year2010
Edition0
Translation No
Refereed No
Webmaster