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


TitleCertifying properties of an efficient functional program for computing Gröbner bases
Author(s) Jose L. Freire, Victor M. Gulias, J. Santiago Jorge
TypeArticle in Journal
AbstractThis paper explores the certification of properties of an efficient functional program in the area of symbolic computation: the calculation of Gröbner basis of a set of multivariate polynomials. Our experience in the development of industrial systems and the certification of some of its relevant properties has led us to use a methodology consisting of functional programs to write the code and the formal verification of fundamental properties. The functional language objective caml has been chosen to implement the program. To verify the properties two approaches are explored: manual proofs that reason directly over the source code of the algorithms, applying techniques like equational reasoning, and theorem provers that are used as a tool to help us certify a model of the real system. The chosen proof assistant is coq. Not only will the certification of the software be taken into consideration but also its efficiency. In addition, we present a graphical interface which eases the use of the program.
KeywordsFormal methods, Software verification, Theorem provers, Functional programming, Gröbner bases, Buchberger’s algorithm
URL http://www.sciencedirect.com/science/article/pii/S0747717108001478
JournalJournal of Symbolic Computation
Pages571 - 582
NoteSpanish National Conference on Computer Algebra
Translation No
Refereed No