Mathias Fleury

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



  • 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



Journal Papers


Conference Papers 


Workshop Abstracts


Formal Proofs

Internship Reports