Stéphane Graham-Lengrand

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