
 
Computer science Professor Doctor at École Nationale Supérieure d’Informatique pour l’Industrie et l’Entreprise (aka Ensiie) which is a french “Grande École” located at Evry in the southern suburbs of Paris.
Member of the Centre d’Études et de Recherches en Informatique (aka Cedric) of Conservatoire National des Arts et Métiers (aka CNAM). I work inside the Conception et Programmation Raisonnée (aka CPR) group of Catherine Dubois.
Former member of LIP6 in the SPI team of Thérèse Hardin, my old page.
My research interests concern computerized mathematics which deals with performing mathematics with a computer.
I began my research in the area of Computer Algebra which is automatic manipulation of mathematical formulas. Daniel Lazard was my thesis advisor and I contributed the LazardRiobooTrager method to integrate rational functions. This is an old but still current algorithm which is described in textbooks like Algorithms for computer algebra by Geddes, Czapor and Labahn or Modern Computer Algebra by Von Zur Gathen and Gerhard. My thesis also contains an enhancement to express an integral in real terms which is described in the Symbolic Integration book of late Manuel Bronstein who refereed my thesis. These algorithms are used by all major computer algebra systems such as the free packages Axiom and Maxima or the commercial Maple and Mathematica.
My thesis was about Cylindrical Algebraic Decomposition (aka CAD) which is a technique to decompose the ndimensional euclidean space into connected regions where the signs of a given set of nvariables polynomials remain constants. I implemented a Regular Axiom package performing CAD. Most of the improvements for CAD were due to a better management of real algebraic numbers. These algorithms were published in ISSAC 92 and Imacs 93. I still maintain the sources for the RECLOS package since NAG Ltd included it in Axiom and it is now part of the distribution. This implementation is still today the only one which solves non trivial problems using a general approach.
My Habilitation was about certification for Computer Algebra software. I am now more concerned with Effective Mathematics and Program Certification where we also reflect mathematical properties and their proofs to the computer. Together with Thérèse Hardin we originated the FoCaL project at LIP6. The project evolved into a collaboration between researchers of INRIA, Cedric and LIP6.
Since my new position the work of the FoCaL project is mostly done at Inria, CedricCNAM together with ENSIIE.
Software reliability can be designed from two paradigms, one is using proof assistants and the other is program annotation. Proof assistants such as Coq, Isabelle or PVS offer languages to design error free programs. Program annotation such as Caduceus or JML offer conservative extensions to existing languages.
Like proof assistants we offer a language and tools to achieve certification. One of the main contributions of FoCaL is that the programmer has a powerfull mecanism to better modularize programs. The concepts of species, collections and entities enable to reduce the gap between an informal human specification and a precise computer checked verification.
See the FoCaL Web page.
Some research topics I participate in are
Selected works
Page “Renaud Rioboo Public Page” was generated using H^{E}V^{E}A is valid html and viewable using any browser 