Patricia Bouyer-Decitre: making safety-critical software more reliable through mathematics

Patricia Bouyer-Decitre is a researcher in computer science in the field of formal methods and director of the “Laboratoire méthodes formelles” (Formal methods laboratory) - LMF (Université Paris-Saclay, ENS Paris-Saclay, CNRS). Her impressive career reveals a researcher who is as humble as she is enthusiastic. 

Patricia Bouyer-Decitre was interested in mathematics from a very early age. She completed a science preparatory course at the “Lycée Chateaubriand” in Rennes before joining the “École normale supérieure de Cachan” in 1996 where she studied for a joint course in mathematics and computer science. “I wanted to be a teacher, so I went on to pass the ‘agrégation’ (teaching qualification) in mathematics.” However, as she was also interested in computer science, she completed a period of study at Aalborg University in Denmark and did an Advanced Studies Diploma (DEA) in that subject, which she followed up with a thesis on the monitoring of time-dependant computer systems (which take into account the dates events occur) at the “Laboratoire spécification et verification” (Specification and verification laboratory) - LSV (Université Paris-Saclay, ENS Paris-Saclay, CNRS). “During this period, I formed very strong friendships and professional contacts - in fact I still work with some of them today. I have very good memories of this thesis!” Patricia Bouyer-Decitre then  gave up on the idea of teaching to concentrate solely on research. She joined CNRS as a research fellow in 2002. She took on the leadership of LSV in 2020, before managing the LMF in January 2021. This laboratory is the result of merging the LSV with the VALS team (Vérification d'algorithmes, de langages et de systèmes - Verification of algorithms, languages and systems) at the “Laboratoire de recherche en informatique” (Computer Science Research Laboratory) - LRI (Université Paris-Saclay, CNRS).

The reliability of safety-critical software

Patricia Bouyer-Decitre’s area of research is that of formal methods for the analysis of computer programmes to prove their reliability and performance. “What I like best about computer science is that it has the same rigour as mathematics, but with an applied focus.” These applications ensure the correct functioning of computer systems, or identify errors in them using mathematical models. This is essential for a lot of the safety-critical software used for avionics, automotive systems and medical devices - the operation of which can have an impact on human lives. It is also important for home automation, democracy and digital health, which are all vulnerable to interference and data theft. 

Award-winning work

Patricia Bouyer-Decitre excels in her field. This has earned her awards and promotions. In 2007, while she was enjoying a secondment year in Oxford thanks to the Marie Skłodowska-Curie European Action Programme awarded to the most promising researchers in their field, she was awarded a bronze medal by CNRS. The medal was in recognition of her work on a widely publicised audit programme in which she identified an error which appeared relatively rarely. “This was a discrete but significant bug in the timed automata analysis algorithm, i.e. in the mechanism underlying the operation of the software.” In 2009, she was appointed Assistant Director of the LSV and in 2010, she successfully passed the research director competitive exam at CNRS. In 2011, the association européenne d’informatique théorique (European Association for Theoretical Computer Science - EATCS) awarded her the European Presburger Award which is given to young scientists who make an outstanding contribution to the field of theoretical computer science. The award was in recognition of all her work since the beginning of her career.

Great strides ahead thanks to an ERC research grant

That same year she applied for an individual research grant from the European Research Council (ERC). Highly prized by the scientific community, this funding targets original pathfinder projects which lead to scientific, technical and societal discoveries. Her application was accepted in 2012 and provided with funds of €1.5 million from 2013 until 2019. “Thanks to this funding, I was able to do some exciting work together with my colleague, Nicolas Markey a researcher at the ‘Institut de recherche en informatique et systèmes aléatoires’ (Institute for Research in Computer Science and Random Systems) - IRISA (Université Paris-Saclay, Inria, CNRS, CentraleSupélec, Université de Rennes) and our PhD students and post-doctoral students.” This mostly concerned the error-free management of uncertainties by computer programmes. An example of this is those faced by aircraft autopilot programmes when they encounter weather hazards and need to adapt their flight plans without any mishap. Another is robot designers when building devices such as mechanical arms whose trajectories must remain controlled and responsive under all conditions. Patricia Bouyer-Decitre’s mission, and that of her colleagues, is therefore to ensure the reliability of the computer systems they analyse using formal methods. That is to say, abstract versions of systems and their behaviour. The latter use mathematical tools such as logic, automata, Markov processes (a type of probability) or models and concepts inspired by game theory. “The challenges are many with this type of research. The right models have to be designed and developed. Once we are satisfied about this, we develop algorithms to analyse their mechanisms.” After these checks, the models are tested on the machines, improved if necessary, and then passed on to industry. 

The researcher and her team collaborate with several other laboratories to carry out their work. Examples include the “Institut des systèmes intelligents et de robotique” (Institute for Intelligent Systems and Robotics – ISIR), IRISA, as well as Aalborg University in Denmark and the University of Mons in Belgium.

Leadership of the LMF

Following the decision of the trustees in 2018 to create a research unit with a focus on formal methods within Université Paris-Saclay, members of LSV and the VALS team at LRI put their faith in Patricia Bouyer-Decitre and Évelyne Contejean to set up the future laboratory’s scientific project. “Our two groups were looking at very similar areas concerning the reliability of safety-critical software. This connection is very important in terms of science. I am delighted to be a part of this venture.” Since the beginning, she has been involved in discussions about and the development of the project. This new stage in her career is also a kind of tribute. “My laboratory gave me the opportunity to do a lot of exciting work. In return, it is right that I help to create an environment which is conducive to generating new research.” LMF came into being on 1 January 2021 and the researcher has great ambitions for this new unit. She hopes to position it as a flagship in its field of research at a national and international level. To attain this, she wishes “to foster a laboratory environment where everyone feels free to develop his or her research and feels as much enthusiasm as I do to do so!”