Picture of me

Mathias Fleury

mathias.fleury@mpi-inf.mpg.de

Physical location: Campus E1 5, Room 640 (6th floor)

+49 681 9325 - 2931, fax - 2999

Max-Planck-Institut für Informatik
Saarland Informatics Campus
Building E1 4
66123 Saarbrücken

 

 

Academic Activity

Research Interest:

  • Theorem proving
  • Formal verification

Education:

Internships:

  • February - June 2015: Formalisation of the resolution, DPLL and CDCL calculi, based on Christoph Weidenbach's upcoming textbook Automated Reasoning — The Art of Generic Problem Solving. Master Thesis.
  • Summer 2014: Sledgehammer is a powerful interface from Isabelle to automated provers, to discharge subgoals that appear during the interactive proofs. It chooses facts related to this goal and asks some automatic provers to find a proof. The proof can be either reconstructed or just used to extract the relevant lemmas: in both cases the proof is not trusted. We extend the support by adding one first-order prover (Zipperposition), the reconstruction for two higher-order ATPs (Leo-II and Satallax) and an SMT solver veriT. The support of higher-order prover should especially improve Sledgehammer's performance for higher-order goals. This internship project took place at the TUM, under the supervision of Jasmin Blanchette. Report.
  • Summer 2013: We present a formalization proof of Uno and Yagiura's algorithm, using the theorem proof assistant Coq. This is a fundamental combinatorial algorithm which operates over permutation. Direct applications include computational biology (e.g. heuristics in estimating the genealogical distance between two species), text processing (e.g. generating the synchronous context-free grammar of two sequences with many-to-many alignment links ), the problem has been generalized to d permutations by Heber and Stoye, ... This internship project took place at LIP6, Université Pierre & Marie Curie, Paris, under the joint supervision of B.M. Bui-Xuan and F. Peschanski.

Draft and Publications

Draft

  • A Verified SAT Solver Framework including Optimization and Partial Valuations
    Mathias Fleury, Christoph Weidenbach, and Dominik Zimmer
    Draft Paper

  • Formalizing logical calculi in Isabelle
    (what will be my dissertation once finalized)
    Latest draft

 

Journal Papers

 

Conference Papers 

  • Optimizing a Verified SAT Solver
    Accepted at NFM 2019, : Badger, J. and Rozier, K.Y (eds) 
    Mathias Fleury
    Draft Paper

  • A Verified SAT Solver with Watched Literals Using Imperative HOL
    Mathias Fleury, Jasmin Blanchette, and Peter Lammich.
    In Andronick, J., Felty, A. P. (eds.) 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 158–171, ACM, 2018. 
    (PDF)
  • Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL
    Jasmin Blanchette, Mathias Fleury, and Dmitriy Traytel.
    In Miller, D. (ed.) 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), LIPIcs 84, pages 11:1–11:18, Schloss Dagstuhl, Leibniz Zentrum für Informatik, 2017,
    Postprint (PDF)
  • Foundational (co)datatypes and (co)recursion for higher-order logic
    Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, and Dmitriy Traytel.
    In Dixon, C., Finger, M. (eds.) 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), LNCS 10483, pp. 3–21, Springer, 2017.
  • A verified SAT solver framework with learn, forget, restart, and incrementality 
    Jasmin Blanchette, Mathias Fleury, and Christoph Weidenbach.
    In Sierra, C. (ed.) 26th International Joint Conference on Artificial Intelligence (IJCAI-17), pp. 4786–4790, ijcai.org, 2017. 
    Postprint (PDF)
  • A verified SAT solver framework with learn, forget, restart and incrementality
    Jasmin Blanchette, Mathias Fleury, and Christoph Weidenbach.
    In Olivetti, N. and Tiwari, A. (eds.) 8th International Joint Conference on Automated Reasoning (IJCAR 2016), Springer, 2016.
    Preprint (PDF), Springer web page

 

Workshop Abstracts

 

Formal Proofs

 

Tutorial

Internship Reports