MSc Jahrim Gabriele Cesario
jahrimgabriele.cesario@unisg.ch
jahrim-gabriele-cesario-288a822b8
0009-0000-1448-5676
jahrim
https://jahrim.github.io

School of Computer Science
Torstrasse 25
9000 St. Gallen, Switzerland

I am a PhD student in the Programming Group since May 2024, after a Master’s degree in Computer Science and Engineering at the University of Bologna.

I am currently researching optimizations for formal verification methods in the field of Programming Languages. In my recent works, I have been focusing on e-graphs, a data structure for encoding equalities, widely used in SMT Solvers and theorem provers.

Publications

1. POPL
   Propel
   

   Dis/Equality Graphs

   George Zakhour, Pascal Weisenburger, Jahrim Gabriele Cesario, Guido Salvaneschi

   Proceedings of the ACM on Programming Languages 8 (POPL), 2025

   Abstract PDF Supp

   E-graphs are a data structure to compactly represent a program space and reason about equality of program terms. E-graphs have been successfully applied to a number of domains, including program optimization and automated theorem proving. In many applications, however, it is necessary to reason about disequality of terms as well as equality. While disequality reasoning can be encoded, direct support for disequalities increases performance and simplifies the metatheory.

   In this paper, we develop a framework independent of a specific implementation to formally reason about e-graphs. For the first time, we prove the equivalence of e-graphs to the reflexive, symmetric, transitive, and congruent closure of the equivalence relation they are expected to encode. We use these results to present the first formalization of an extension of e-graphs that directly supports disequalities and prove an analytical result about their superior efficiency compared to embedding techniques that are commonly used in SMT solvers and automated verifiers. We further profile an SMT solver and find that it spends a measurable amount of time handling disequalities.

   We implement our approach in an extension to egg, a popular e-graph Rust library. We evaluate our solution in an SMT solver and an automated theorem prover using standard benchmarks. The results indicate that direct support for disequalities outperforms other encodings based on equality embedding, confirming the results obtained analytically.