Évelyne Contejean: Avoiding computer bugs

Évelyne Contejean is a CNRS Research Director at the Formal Methods Laboratory (LMF - Univ. Paris-Saclay, CNRS, ENS Paris-Saclay, CentraleSupélec, Inria). She specialises in automatic demonstration and proof assistants. This field of computer science research focuses on designing efficient tools to thwart all potential bugs in the digital ecosystem at an early stage.

Since 2018, Évelyne Contejean has been actively involved in the creation of the Formal Methods Laboratory, of which she became Deputy Director when it opened in 2021. This laboratory brings together around 50 permanent researchers, mainly from the Laboratory for Computer Science (LRI - CNRS, Univ. Paris-Saclay) and the Specification and Verification Laboratory (LSV - CNRS, ENS Paris-Saclay). "Formal methods are a set of techniques that analyse our digital world," says the researcher. "We use them to provide guarantees about the proper functioning and reliability of various IT objects, such as programmes, software, protocols and systems." The objective is to provide upstream "proof", as much as possible, that there will be no bugs, to avoid failures such as the Ariane 5 launch in 1996, which Évelyne Contejean's colleagues were asked to analyse.

Automatic rewriting and demonstration 

Computer proofs involve logic and "discrete" mathematics. Rewriting is a method of dealing with equality in proofs. It is a computational model that models programming languages in particular. Évelyne Contejean rewrites the mathematical equations to deduce others, with the aim of automating the process. "The principle is that when I know that two expressions are equal, I can replace the ‘larger’ by the ‘smaller’, by which I mean, calculate partially in a very complicated equation. The two essential properties of a ‘good’ rewriting system are confluence, which ensures that every way of computing gives the same result, and termination, which guarantees that the process stops in a finite time. The idea is to provide the end user with a tool that, from the description of the problem in the form of equations, allows them to press a button to obtain a result in the shortest possible time."

The logic of a proof-oriented path

Évelyne Contejean loved mathematics and took the entrance exam for the Grandes Ecoles in Besançon; she was admitted to the ENS in Fontenay-aux-Roses in 1984. There, she continued her university career while preparing for the 'agrégation' (a teaching certificate) in mathematics. At the same time, reading the book "Gödel, Escher, Bach" by Douglas Hofstadter introduced her to the world of logic. In 1988, having passed her 'agrégation', the young scientist turned to computer science research. She did her Master's internship at the Laboratory for Computer Science in Orsay and then, thanks to a grant, began writing a thesis on the rewriting of mathematical equations, which she defended in 1992. 

In 1993, after a one-year post-doc at the Max Planck Institute in Saarbrücken, still in the field of automatic demonstration, she was recruited as a research fellow at CNRS. She obtained her HDR (Accreditation to Supervise Research) in 2014 and became Director of Research in 2019.

Alt-Ergo or the opportunity to obtain proof

In 2011, Évelyne Contejean and her colleagues developed a new tool by managing to take into account non-orientable equalities in SMT (satisfiability modulo theories) theorem provers. "This work ranged from theory to the creation of a tool, Alt-Ergo, which is now used to obtain proofs in a large number of fields." This research was rewarded by the European Association for Theoretical Computer Science (EATCS) prize, awarded by the European ETAPS federation during the Conferences on Theory and Practice of Software.

To end or not to end

In the early 2000s, computer science researchers from different countries (France, Germany, the Netherlands, the United States) engaged in competitions to finish rewriting systems using interposed tools: since rewriting replaces - in principle - large expressions with smaller ones, it must be possible to demonstrate that the process ends. This is the purpose of automatic termination analysis tools. But a decade later, two tools contradicted each other. Évelyne Contejean then had the idea of guaranteeing the results of these tools. She became caught up in the work and developed interactive proofs of termination criteria in the Coq proof assistant. "The proofs are extremely detailed, each step is explained and each proof is double-checked by computer. This very detailed analysis allows us to optimise the proof even if it has already been demonstrated before with paper and pencil."

The usefulness of proof assistants

Proof assistants make more secure and more sophisticated proofs than automatic demonstrators. "The proofs obtained quickly and automatically use relatively simple theories. If we want to look at more complicated concepts, we have to use human intelligence." These proofs are built interactively with a computer. "Once the proof is established, the proof assistants verify that we have analysed all the cases and that we are not mistaken in the logical sequences."

Évelyne Contejean then had the idea of applying formal methods to other objects, such as data-centric languages, the speciality of her colleague Véronique Benzaken, with whom she has been collaborating for around ten years. "The results can be more or less substantiated depending on the field of computer science. When we use a proof assistant, we get strong guarantees." This research is part of the DataCert project, which was supported by the ANR and ended in 2021.

A certified compiler

Today, Évelyne Contejean is working on the development of a verified compiler for SQL (Structured Query Language), the most widely used data management language. "SQL takes a user's queries and rewrites them into an executable plan. But this transformation is neither obvious nor immediate. Current SQL engines have a number of recipes for this transformation, but there is no guarantee that they are correct, except that they have been in use for a long time," says the researcher. Not only does Évelyne Contejean formally check the most well-known transformations, but she will also propose new ones. "‘Intimately’ entering into the proofs leads to better understanding and the possibility of improving them, simplifying them or discovering new theorems."

Through her research and her involvement in different structures (CoNRS, Comue Université Paris-Saclay, laboratory), Évelyne Contejean enjoys the freedom of her profession while advocating a certain vision of her field of computer science research. "Like Galileo, who wanted to study nature with mathematics, I propose studying the digital world with formal methods," she concludes.