Bibliographic Details
| Title: |
A verified Common Lisp implementation of Buchberger’s algorithm in ACL2 |
| Authors: |
Medina-Bulo, Inmaculada1 http://neptuno.uca.es/~inmame, Palomo-Lozano, Francisco1 http://neptuno.uca.es/~palomo, Ruiz-Reina, José-Luis2 http://www.cs.us.es/~jruiz |
| Source: |
Journal of Symbolic Computation. Jan2010, Vol. 45 Issue 1, p96-123. 28p. |
| Subjects: |
COMMON LISP (Computer program language), Algorithms, ACL (Computer program language), Polynomials, Programming languages, Software verification, Algebra software |
| Abstract: |
Abstract: 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. [Copyright &y& Elsevier] |
|
Copyright of Journal of Symbolic Computation is the property of Academic Press Inc. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
