Internship proposals

The PROTHEO project aims at designing and implementing tools for specifying, proving and verifying programs. Computations and deductions are modelized by using the concepts of rules, constraints and strategies. This declarative and executable formalism allows us to specify, prototype and verify software components. We develop a prototyping environment and proof techniques for verifying program properties.

The project has three strongly connected research themes: constraints, rewriting and automated deduction. In particular, we use constraint and rewriting techniques to improve the efficiency of proof assistants and we formalize constraint solvers and theorem provers with rewrite rules controlled by strategies.

The software developped in the project (ELAN, TOM, Cariboo, GasEl) allow us to validate our ideas, present them to the community and transfer our knowledge towards application domains.

The following 4 month internship proposal concerns engineering school students The following Master internships (DEA is a kind of french master oriented to research) are an initiation to research in the team that may lead to a PhD.