Students

PhD thesis offer from September 2020

  • "Using Concurrency for First-Order Analytic Tableaux" [description]

Internship Offer for 2019/2020

  • "Using Concurrency for First-Order Analytic Tableaux" [description]
  • "Deductive Approaches for Process Verification" [description] (in French)

Current PhD Students

  • Vincent Iampietro, from September 2018.
    "Formal verification of a methodology for the design
    and production of critical digital systems    ".
  • Alexandre Le Borgne, from October 2016.
    "ARIANE: Automated Re-documentation to Improve
    software Architecture uNderstanding and Evolution    ".

Former PhD Students

  • Guillaume Bury, defended on January 2019.
    "Integrating Rewriting, Tableau and Superposition into SMT".
  • 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".