Certifying properties of an efficient functional program for computing Grobner bases

This paper explores the certification of properties of an efficient functional program in the area of Symbolic computation: the calculation of Grobner 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 LIS 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 LIS 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. (C) 2008 Elsevier Ltd. All rights reserved.