Internship Offer for 2018/2019

  • "Use of Machine Learning Techniques to Help Find Proofs
    in the Coq Proof Assistant"
    [description] (in French)
  • "Deductive Approaches for Process Verification" [description] (in French)

Current PhD Students

Former PhD Students

  • Pierre Halmagrand, defended on December 2016.
    "Automated Deduction Modulo".
  • Pierre-Nicolas Tollitte, defended on December 2013.
    "Extracting Certified Functional Code from Inductive Specifications".
  • Mélanie Jacquel, defended on April 2013, in collaboration with Siemens.
    "Designing an Environment to verify Atelier B Proof Rules".
  • Jean-Frédéric Étienne, defended on July 2008.
    "Certifying Airport Security Regulations using the Focal Environment".

Former Master Thesis Students

  • Guillaume Bury, 2014.
    "Arithmetic Automated Proofs in Sequent Calculus".
  • Pierre Halmagrand, 2013.
    "Extending the Zenon Automated Theorem Prover with Deduction Modulo".
  • Martin Keogh, 2011.
    "User Interface for the BCARe Tool".
  • Benjamin Lalière, 2009.
    "Implementation of a Parser for OpenMath".
  • Sanaa Toumi, 2009.
    "Using CAD to Test First-Order Formulas over Real Closed Fields in the Focal Environment".
  • Pierre-Nicolas Tollitte, 2009.
    "Producing Certified Funtional Code from Inductive Specifications in the Focal Environment".
  • Nicolas Bertaux, 2008.
    "A Module-Based Compilation Scheme for the Focal Environement".
  • Yuan Gang, 2003.
    "Compilation Schemes for the Focal Environment".