I am a computer science postdoc at the University of Iowa, where I study SMT solving and work on the solver cvc5. My main research interest is making SMT solver more useful by using expressive type systems. Currently, I am focusing on SMT proof certificates. These certificates must be easy to produce, and easy to check. To solve both goals, we use logical frameworks.
Concretely, we are currently building the Eunoia language that combines ideas from the LFSC framework with the familiar syntax of the Alethe format.
SMT research is driven by solver development and empirical evaluations. I am a developer of cvc5, and the lead developer veriT. I also co-maintain the SMT-LIB benchmark library, and participated in the SMT competition.
My PhD at the Inria Centre at Université de Lorraine was supervised by Pascal Fontaine, Jasmin Blanchette, and Stephan Merz. I worked on the integration of veriT into Isabelle/HOL. This led to the specification of the universal proof format Alethe. I also studied quantifier instantiation and strategy scheduling.
Beyond research, I am passionate about teaching. I taught applied computer science at Polytech Nancy (in French), and undergraduate classes at the University of Iowa.
Color code: Conference Refereed workshop Thesis Informal publication
The arrow (↑) denotes that the authors are in alphabetic order, (↓) denotes reverse alphabetic order.
This section lists most of my recent talks.
2025, January 14
CODAG Seminar, Université de Caen, Caen, Normandy. France
2024, March 7
CS Extras, Grinnell College, Grinnell, IA. USA
2023, May 12
EuroProofNet COST Action, University of Liège, Liège. Belgium
2021, July 11
PxTP, affiliated with CADE-28, Virtual
2021, July 18
SMT, affiliated with CADE-28, Virtual
2021, July 18
SMT, affiliated with CADE-28, Virtual
2019, April 10
AITP, University of Innsbruck, Obergurgl, Austria
Program Committee: SMT
Artifact Evaluation Committee: ATVA
Reviews: TACAS
Program Committee: SBMF
Artifact Evaluation Committee: ICFP ATVA TACAS
Reviews: Sci. Comput. Program. J. Autom. Reason.
Program Committee: SMT
Reviews: FroCoS
Artifact Evaluation Committee: TACAS
Reviews: TACAS SMT Int. J. Softw. Tools Technol. Transf.
Spring 2025
CS:3820 Programming Language Concepts
3 creditslectures, weekly homework assignments, and office hours
Undergraduate level introduction to basic ideas from the study of programming languages, such as semantics and type systems. The course also serves as introduction to Haskell.
Fall 2024
CS:3820 Programming Language Concepts
3 creditslectures, weekly homework assignments, and office hours
Undergraduate level introduction to basic ideas from the study of programming languages, such as semantics and type systems. The course also serves as introduction to Haskell.
Spring 2024
CS:4350 Logic in Computer Science
3 creditslectures, biweekly homework assignments, and office hours
Received a Thank-a-Teacher Letter.Introduction to formal logic, and its applications in computer science. This in included SAT solving, and model checking.
Fall 2023
CS:3330 Algorithms
3 creditslectures, biweekly homework assignments, and office hours
Recognized by the graduating class of 2023.Undergraduate algorithms course, with a focus on recursion as a general concept. Classic algorithms, such as Quicksort, were introduced as case studies for recursion.
Spring 2023
CS:4350 Logic in Computer Science
3 creditslectures, biweekly homework assignments, and office hours
Introduction to formal logic, and its applications in computer science. This in included SAT solving, and model checking.
Spring 2022
Projet informatique
18h TPproject guidance, office hours, and grading.
Team based software engineering project
Spring 2022
Programmation algorithmique II
44h TDguided exercises
Exercise sessions for a class introducing basic algorithms, and complexity theory.
Fall 2021
Systèmes distribués (API web)
12h CM 24h TDlectures, and guided exercises
Introduction to REST APIs. Students learned to perform simple API queries using Unix tools, to implement complex API clients in Java, and to develop REST API services.
Fall 2021
Programmation distribuée & Web avancée
24h CM 28h TDlectures, and guided exercises
Introduction to micro service architectures. The student learned the theoretical ideas behind micro services, and practised implementing and documenting a micro service system in Java Spring.
Spring 2017
Juggling
exercise sessions
Instructor for the juggling course offered by university sports.
Fall 2016
Juggling
exercise sessions
Instructor for the juggling course offered by university sports.
Spring 2016
Theorem Proving in Isabelle/HOL
exercise sessions
Interdisciplinary course “Computational Metaphysics”.
Jakob Bleier Marie Duflot-Kremer Mathias Fleury Pascal Fontaine Christa Jenkins Hanna Lachnitt Pierre Lermusiaux Andrew Marmaduke J. Garrett Morris Mathias Preiner Martin Riener glitch.love Andy Reynolds Cesare Tinelli Sophie Tourret Athénaïs Vaginay Haniel Barbosa Yoni Zohar