An FNRS Research Fellowship for Tom CLARA to Develop Decision Procedures in Logic Using Automata
His background
Tom CLARA began his studies in civil engineering at the University of Liège in 2020. Initially broadly interested in mathematics and physics, he quickly developed a particular interest in computer science. After earning his bachelor’s degree, he pursued a master’s degree in data science engineering. During his master’s thesis, he discovered with enthusiasm a more theoretical side of computer science. Tom won the award for best master’s thesis in data science from AIM (Association of Alumni of the Montefiore Institute). His master’s thesis was also awarded by NRB. He published a first paper in the framework of the 29th International Conference on Implementation and Application of Automata (Italy – April 2025).
Encouraged by these experiences, Tom chose to pursue along this path.
So, together with the Professors Bernard Boigelot and Pascal Fontaine, his future supervisors, he decided to apply for an FNRS Research Fellowship. Obtaining this fellowship allowed him to start his research in October 2025.
His research
Software Verification
When a computer program plays a critical role in a system (for example, in an airplane), it is often necessary to ensure that the program is reliable. Software verification is the field of computer science that develops methods for analyzing programs and guaranteeing certain of their properties. A common approach in this field consists in encoding the behavior of a system (for example, the interaction between an environment and a program) as a logical formula that formally describes it. Studying the behavior of the system then reduces to a simpler problem: determining whether the associated formula can be made true or not. Hence the need to design methods—called decision procedures —that can answer this question.
Automata-Based Decision Procedures
Tom’s research focuses primarily on developing new decision procedures for certain logics that involve real or rational variables. A promising but underused approach in this context relies on fascinating mathematical objects known as automata. These objects have the advantage of being easily manipulable (even by a computer) while maintaining high expressive power.
A Blend of Theory, Practice, and Related Disciplines
Tom’s project combines both theory and practice. It involves first studying and understanding the mathematical properties of advanced types of automata, then designing efficient algorithms to manipulate them, and finally implementing a decision procedure based on these algorithms. The main challenge lies in making this procedure practical and usable. Such a procedure could have interesting applications not only in software verification but also in several related areas of logic, including automated reasoning, the development of SMT solvers (these solvers aim at solving the problem of satisfiability modulo theories, which is the problem of deciding whether a logical formula in some theory can be made true), and more generally symbolic artificial intelligence (that gathers the methods based on a symbolic representation of problems, for instance thanks to logic).
