PROTHEO Research team

Activity reports

Introduction

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:

Constraint solving,

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.

Inria Headquarters and research centres

Direct links

Social