Robin Coutelier is the recipient of the Paul Gochet Award 2024

Robin Coutelier, who holds a Master's degree in Civil Engineering in Computer Science and is currently a PhD student at the Technische Universität Wien (TU Wien), is the recipient of the Paul Gochet Award attributed by the University of Liège Foundation. He was awarded the prize for his Master thesis on automated theorem provers. His research focuses on automated reasoning and, more specifically, on the design of computer programmes capable of solving tasks requiring logical reasoning.

I

n a world where computer science plays a crucial role in many areas, from computer models to software design, a little-known but essential technology is emerging: automated theorem provers. These computer programmes are designed to prove the validity of a logical formula based on formal rules of reasoning. Program verification often reduces to formula validity checking.  Therefore, it is possible to use an automated theorem prover, such as Vampire, cvc5 or Z3, to check the correctness of programmes. It is in this highly specialised field that Robin Coutelier has focused his research.

During his Master's degree in Civil Engineering in Computer Science from ULiège in 2023, Robin Coutelier developed a passion for elegant algorithms early on when attending the Algorithms and Data Structures course taught by Prof. Pascal Fontaine.  He then discovered a deep interest in satisfiability solvers for Boolean formulae, a problem, seemingly very abstract, that turns out to have a considerable impact in computer science, particularly in relation to the famous open problem P≟NP. 

‘The subject of his Master thesis - Chronological vs. non-chronological backtracking in satisfiability modulo theories - explores chronological backtracking in SMT (Satisfiability modulo theories) solvers,’ explains Prof. Pascal Fontaine, who supervised the thesis. ‘He examined recent chronological backtracking techniques within the propositional solver embedded into a satisfiability modulo theories solver, as an alternative to non-chronological backtracking which is traditionally used’. It was for this work that Robin Coutelier was awarded the Paul Gochet 2024 prize. "I feel very honoured that the Paul Gochet Prize committee granted me with the 2024 Prize. This prize will enable me to continue my research in collaboration with the University of Liège, on automated theorem proving and SMT solvers’, Robin Coutelier is delighted to say. 

Robin Coutelier is currently a PhD student at the Technical University of Vienna (TU Wien) under the supervision of Prof. Laura Kovács. His research is a continuation of his work on automated reasoning, with a particular focus on the Vampire prover, which has dominated first-order proof competitions for several years.   A promissing future indeed, joining an excellent group in Vienna, the craddle of modern logic in Europe.

See Robin Coutelier's Master thesis

The Paul Gochet Foundation

The Fondation Gochet rewards Master or PhD theses in the field of logic, i.e. the science of reasoning methods, their formalisation and automation. The recipient must be pursuing research in logic and must either have completed all or part of a previous course of study at the University of Liège or have future research to carry out at the University of Liège.