Students
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
- Alexandre Le Borgne,
from October 2016.
"Evolution and Reuse of Component-Based Software Architectures". - Guillaume Bury, from October
2014.
"SMT Modulo".
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".