On this page, I list all my talks and slides. Remark that several
talks are impossible to understand without me talking (this is half of
the point of the talk: someone is talking).
2024
- Mathias Fleury and Bruno Andreotti Alethe, A flexible proof format with fine-grained steps
2023
- Mathias Fleury, in front the Professors (informal talk, towards the habilitation)
- Mathias Fleury and Peter Lammich, Porting IsaSAT to LLVM (and Inprocessing)
- Mathias Fleury, MDX Isabelle Summer School
2022
- Mathias Fleury, Verifying Solvers: How Much Do You Want to Prove?
- Mathias Fleury, Discussion: How to compare techniques in solvers? And how to write such a solver? (work-in-progress with Armin Biere and Karem Sakallah)
2021
- Mathias Fleury and Armin Biere, Efficient All-UIP Learned Clause Minimization.
- Mathias Fleury and Christoph Weidenbach. A Verified SAT Solver Framework including Optimization and Partial Valuations
2020
- Armin Biere and Mathias Fleury, Chasing Target Phases
| POS'20 |
slides |
| 11th Workshop on Pragmatics of SAT (POS'20) |
video |
- Mathias Fleury, One Thousand and One Refinement: From CDCL to a Verified SAT Solver
2019
- Reconstructing veriT proofs in Isabelle/HOL
| UPSCaLe meeting |
slides |
| Paris, November 29, 2019 |
|
- Fleury and Weidenbach, Extending an Isabelle Formalisation of CDCL to Optimising CDCL
2018
- Blanchette, Fleury, Lammich, and Weidenbach, A Verified SAT Solver with Watched Literals Using Imperative HOL
- Fleury, Blanchette, and Fleury, A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract)
2017
- Blanchette, Fleury, and Traytel, Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
- Blanchette, Fleury, Lammich, and Weidenbach, A Verified SAT Solver with Watched Literals Using Imperative HOL
- Blanchette, Fleury, and Weidenbach, A Verified SAT Solver Framework
2015
- Fleury, Formalisation of Ground Inference Systems in Isabelle