PROTHEO Research team
The PROTHEO project aims at designing and implementing tools for program specification, proof of properties and safe and efficient execution.
We are working on environments for prototyping such tools, on theorem provers specialized in proofs by induction and equational first-order proofs, on proof techniques involving constraints and rewrite rules. The project has three strongly connected research domains:
Mechanized deduction with rewrite rules and strategies,
Theorem proving based on deduction modulo.
The team develops and maintains several software packages detailed later in this document. They allow us to test our ideas and results as well as to make them available to the community.
The team PROTHEO
is stopped since 12/31/2007