| 2025 | CADE | Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. | Enrico Lipparini, Thomas Hader, Ahmed Irfan, Stphane Graham-Lengrand |
| 2025 | CAV | Decision Heuristics in MCSat. | Thomas Hader, Ahmed Irfan, Stphane Graham-Lengrand |
| 2024 | IJCAR | MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). | Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stphane Graham-Lengrand, Laura Kovcs |
| 2023 | CADE | QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. | Maria Paola Bonacina, Stphane Graham-Lengrand, Christophe Vauthier |
| 2023 | CCS | Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge. | Samuel Dittmer, Karim Eldefrawy, Stphane Graham-Lengrand, Steve Lu, Rafail Ostrovsky, Vitor Pereira |
| 2021 | CCS | Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. | Jos Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira |
| 2020 | CADE | Solving Bitvectors with MCSAT: Explanations from Bits and Pieces. | Stphane Graham-Lengrand, Dejan Jovanovic, Bruno Dutertre |
| 2019 | TABLEAUX | A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic. | Camillo Fiorentini, Rajeev Gor, Stphane Graham-Lengrand |
| 2018 | CPP | Proofs in conflict-driven theory combination. | Maria Paola Bonacina, Stphane Graham-Lengrand, Natarajan Shankar |
| 2017 | CADE | Satisfiability Modulo Theories and Assignments. | Maria Paola Bonacina, Stphane Graham-Lengrand, Natarajan Shankar |
| 2013 | TABLEAUX | Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture. | Stphane Graham-Lengrand |