A verified Common Lisp implementation of Buchberger’s algorithm in ACL2 |
| |
Authors: | Inmaculada Medina-Bulo Francisco Palomo-Lozano Jos-Luis Ruiz-Reina |
| |
Affiliation: | aEscuela Superior de Ingeniería, Calle Chile s/n 11003 Cádiz, Spain;bETS de Ingeniería Informática, Avda. Reina Mercedes s/n 41012 Sevilla, Spain |
| |
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. |
| |
Keywords: | Formal verification ACL2" target="_blank">ACL2 Computer Algebra Buchberger’ s algorithm |
本文献已被 ScienceDirect 等数据库收录! |
|