Stéphane Graham-Lengrand

Publication Activity (10 Years)

Years Active: 2013-2024
Publications (10 Years): 23

Top Topics

Modulo Theories

Propositional Logic

Top Venues

J. Autom. Reason.

Publications

Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács
MCSat-based Finite Field Reasoning in the Yices2 SMT Solver. CoRR (2024)
Ahmed Irfan, Stéphane Graham-Lengrand
Arrays Reasoning in MCSat. SMT@CAV (2024)
Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács
MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). IJCAR (1) (2024)
Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. CADE (2023)
Samuel Dittmer, Karim Eldefrawy, Stéphane Graham-Lengrand, Steve Lu, Rafail Ostrovsky, Vitor Pereira
Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge. IACR Cryptol. ePrint Arch. 2023 (2023)
Samuel Dittmer, Karim Eldefrawy, Stéphane Graham-Lengrand, Steve Lu, Rafail Ostrovsky, Vitor Pereira
Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge. CCS (2023)
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs. J. Autom. Reason. 66 (1) (2022)
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length. SMT (2022)
Salwa Tabet Gonzalez, Stéphane Graham-Lengrand, Julien Narboux, Natarajan Shankar
Semantic parsing of geometry statements using supervised machine learning on synthetic data. CICM Workshops (2021)
José Carlos Bacelar Almeida, Manuel Barbosa, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. CoRR (2021)
José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. CCS (2021)
José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. IACR Cryptol. ePrint Arch. 2021 (2021)
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness. J. Autom. Reason. 64 (3) (2020)
Stéphane Graham-Lengrand, Dejan Jovanovic, Bruno Dutertre
Solving Bitvectors with MCSAT: Explanations from Bits and Pieces. IJCAR (1) (2020)
Stéphane Graham-Lengrand, Dejan Jovanovic, Bruno Dutertre
Solving bitvectors with MCSAT: explanations from bits and pieces (long version). CoRR (2020)
Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner
Tight typings and split bounds, fully developed. J. Funct. Program. 30 (2020)
Camillo Fiorentini, Rajeev Goré, Stéphane Graham-Lengrand
A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic. TABLEAUX (2019)
Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner
Tight Typings and Split Bounds. CoRR (2018)
Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner
Tight typings and split bounds. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
Proofs in conflict-driven theory combination. CPP (2018)
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
Satisfiability Modulo Theories and Assignments. CADE (2017)
Stéphane Graham-Lengrand, Dejan Jovanovic
An MCSAT treatment of Bit-Vectors. SMT (2017)
Didier Galmiche, Stéphane Graham-Lengrand
Special Issue on Computational Logic in Honour of Roy Dyckhoff. J. Log. Comput. 26 (2) (2016)
Stéphane Graham-Lengrand
Realisability semantics of abstract focussing, formalised. WoF'15 (2015)
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin
Axiomatic Constraint Systems for Proof Search Modulo Theories. FroCos (2015)
Stéphane Graham-Lengrand
Polarities & Focussing: a journey from Realisability to Automated Reasoning. CoRR (2014)
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin
Axiomatisation of constraint systems to specify a tableaux calculus modulo theories. CoRR (2014)
Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi
) and a proof-search strategy for the focused sequent calculus. LFMTP (2013)
Mahfuza Farooque, Stéphane Graham-Lengrand
Sequent Calculi with procedure calls CoRR (2013)
Stéphane Graham-Lengrand
Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture. TABLEAUX (2013)
Alexis Bernadet, Stéphane Graham-Lengrand
A simple presentation of the effective topos. CoRR (2013)