Curriculum Vitae

Intro

I am a Belgian Ph.D student at the TU Wien in the ForSyte group under the supervision of Pr. Laura Kovács. I graduated Magna Cum Laude in 2023 from the University of Liège in Belgium with a master's degree in computer science and engineering.
Though artificial intelligence and machine learning was a big part of my degree, I particularly enjoy working in formal methods and automated reasoning.

I find beauty in the emergence of complex properties from a simple set of rules. For that reason, I am a big fan of strategy board games such as chess and Go. Computer science, and logic in particular is a perfect example of this phenomenon.

Education

Oct 2023 - Now, Ph.D in Computer Science, TU Wien, Austria

Research on efficient data structures and algorithms for automated reasoning.

Sept 2021 - Sept 2023, Master in Computer Science and Engineering, University of Liège, Belgium

Professional focus on Intelligent Systems.
Thesis title: "Chronological vs. Non-Chronological Backtracking in SMT solving.

Sept 2018 - Jun 2021, Bachelor in Engineering, University of Liège, Belgium

Major in Computer Science and minor in Mechanical Engineering.

Aug 2017 - Jul 2018, Chinese language, Yunnan Normal University

I studied the Chinese language in China for a year. I passed HSK4 in 2018.

Languages

  • French: Native
  • English: Fluent
  • Chinese: Intermediate
  • German: Beginner

Work

Research

Ongoing Projects

I am part of the Vampire team and am interested in the theoretical and practical aspects of First-Order Theorem Proving.

Further, I am maintaining NapSAT, a SAT solver written to support variants of Chronological Backtracking. We are working in collaboration with Pascal Fontaine at the University of Liège to integrate NapSAT in an SMT solver.

I started working on a probability reasoner for SMT solvers. The goal is to assert whether some probabilistic statements are consistent or not. In the latter, the module should be able to provide a conflicting clause summarizing the inconsistency. There is unfortunately no public implementation yet, since the project is still in its infancy.

Finished projects

During my research internship at the TU Wien, and during my first year of Ph.D., I worked on the Vampire automated theorem prover's Subsumption and Subsumption Resolution procedures. We improved the speed of the inference engine by 34% using a tailored SAT encoding. The results were presented at CADE-29 (here) and an extended version was accepted for publication in the FMSD journal (camera ready)

During my master thesis and my first year of Ph.D., I specialized in Chronological Backtracking (CB) in SAT solving. I developed a new SAT solver from scratch, NapSAT. We developed a new variant of CB called "Lazy Strong Chronological Backtracking" that was published at SAT (here). We also collaborated with the University of Freiburg to implement this technique in CaDiCaL.

Community Service

  • 2024, Local helper for the 18th International Conference on Reachability Problems, hosted in Vienna
  • 2024, Subreviewer for SCSS 2024

Scientific Activities

  • Sep 2024, 16th Alpine Verification Meeting
    I presented the debugging interface of NapSAT to advocate the observer pattern for debugging complex algorithms.
  • Aug 2024, 27th International Conference on Theory and Applications of Satisfiability Testing
    I presented our paper on lazy reimplication in chronological backtracking at the SAT conference in India.
  • Aug 2024, 15th Pragmatics of SAT International Workshop
    I presented a rediscovery of the linked-list representation of watch lists in SAT solving and discuss why it does not work in practice.
  • Aug 2024, Marktoberdorf Summer School I followed the Summer School on Formal Methods in Herrsching, Germany. The lectures were related to deductive verification, test generation, static program analysis, automated reasoning, modeling, program synthesis,...
  • Jul 2024, 12th International Joint Conference on Automated Reasoning
    I attended the conference in Nancy, France. I did not present any paper but followed the talks.
  • Jul 2024, 8th Vampire Workshop
    I presented the improvements on the method for subsumption resolution made for the FMSD journal. The workshop was collocated with IJCAR 2024 in Nancy.
  • Jun 2024, VeriDis Retreat
    I presented some of my work on SAT solving and Vampire and participated in the scientific conversations. A few ideas emerges from the retreat.
  • Mar 2024, Workshop on Alignment of Proof Systems and Machine Learning
    The Workshop on Alignment of Proof Systems and Machine Learning was organized at the TU Wien. I attended the workshop and presented a machine learning approach for encoding selection in the Vampire theorem prover.
  • Jul 2023, 29th International Conference on Automated Deduction
    After my internship at the TU Wien, we wrote a paper based on the results of the internship. I had the honor of presenting the paper at CADE-29 in July 2023.
  • Jul 2023, 7th Vampire Workshop
    During the Vampire workshop organized during CADE-29, I presented a list of engineering challenges in the development process in Vampire. Though a lot of questions remained open, the discussion was fruitful.
  • Jul 2023, VeriDis Retreat
    For the second time at the VeriDis retreat, I could present some of my work in Vampire and discuss with experts in the field. I was gratifying to see the progression between my first and second attendance.
  • Oct 2021, VTSA Summer School
    I attended the The summer school on verification technology, systems & applications summer school in 2021 in Liège. I was still a Bachelor student at the time, but it was a great opportunity to discover the world of Ph.D students and researchers. It strengthened my motivation to pursue a Ph.D.
  • Jul 2021, VeriDis Retreat
    Prof. Pascal Fontaine invited me to take part in the VeriDis retreat. While I was clearly out of my depth in terms of technical knowledge. It was still very interesting to see what research looks like. I am really grateful to Prof. Pascal Fontaine for motivating me into starting a Ph.D.

Publications

Talks

Awards

  • 2023. Best master thesis in computer science and engineering at the University of Liège in 2023
  • 2023. Best master thesis in computer science and engineering awarded by the AIM and Deuse
  • 2023. Woody Bledsoe award for student's submissions at CADE29
  • 2021. Finalist in the Belgian BCG strategy cup (more than 600 contestants in teams of 3)
  • 2019. 7th place in Europe in the Chinese Bridge international contest for college students
  • 2019. 2nd place in the Belgian Chinese Bridge speech contest for college students
  • 2018. 2nd place in the Yunnan Normal University Chinese speech contest for college students studying Chinese abroad
  • 2016. Was granted a Confucius Institute scholarship for the qualification to the international Chinese Bridge speech contest for high school students

Teaching

Teaching at the TU Wien

Logics and Reasoning for Computer Science

I am a teaching assistant for the course of "Logics and Reasoning for Computer Science" at the TU Wien by Pr. Agata Ciabattoni, Pr. Laura Kovács and Pr. Magdalena Ortiz. Being the team lead for the propositional logic part of the course, I am responsible for the quizzes, exercises and coordinating the final exam for the first part. I also give the first block of exercise sessions.

We use online quizzes for continuous evaluation of the students. As such, and for scalability, I am using a script of my own design to generate hundreds of questions. For obvious reasons, the script is not publicly available, but I am happy to share it with a professor or teaching assistant who would like to use it. Just send me an email.

Teaching at University of Liège

I was a tutor for several classes during my studies, both in English and in French. Here are some of the classes I tutored:
  • 2023: Organisation des ordinateurs by Pr. Bernard Boigelot*
  • 2022-2023: Parallel programming by Pr. Pascal Fontaine
  • 2022: Complément d'informatique by Pr. Pierre Geurts*
  • 2021: Heat Transfer by Pr. Pierre Dewallef and Pr. Vincent Terrapon
  • 2020: Physique II: Electricité et électromagnétisme by Pr. Hervé Caps*
* The classes were in French.

Hobbies

Chess

I have been chess enthusiast since I was 3 or 4 years old, and was a member of the Namur Royal Échecs between 2015 and 2023. I am rated about 1800 FIDE and peaked at 2135 in Blitz on chess.com.

I love Chess for its simple set of rules. And yet, some beautiful tactics of almost unlimited complexity emerge on the 64 squares.

Clarinet

I have been playing the clarinet since I was 8. I was a member of the Orchestre Etudiant des Ingénieurs de Liège between 2018 and 2023.

Unfortunately, I do not play in an orchestra since I moved to Vienna. But I will start looking for one as soon as my German is good enough.

Tabletop Role Playing Games

I started playing Dungeons and Dragons 3.5e when I was a teenager. I now mostly play the role of Dungeon Master in the system DnD 5e. I have the pleasure to play weekly with a group of friends.

German

Since I am currently living in Vienna, I am learning German. I am currently at the A2 level.

Magic and Cardistry

Although I do not perform as much as I used to, I still enjoy fidgeting with cards. I practiced a lot during my year in China, since it was a great ice breaker.