PROTHEO Research team
Constraints, automatic deduction and software properties proofs
- Leader : Claude Kirchner
- Research center(s) : Nancy - Grand Est
- Field : Symbolic systems
- Theme : Reliability and safety of software
The PROTHEO project-team aims at designing and implementing tools for program specification and verification.
We are working on an environment for prototyping such tools, on theorem provers specialised in proofs by induction and equational first-order proofs, on proof techniques involving constraints and rewrite rules. The project has three strongly connected research themes: constraint solving, mechanised deduction with rewrite rules and strategies, and theorem proving.
- Constraint solving.
- Constraint satisfiability on symbolic and numerical domains.
- Collaboration of constraint solvers.
- Constraint satisfaction techniques.
- Mechanised deduction with rewrite rules and strategies.
- Strategy language for constraint solvers and theorem provers.
- Non-deterministic computations.
- Compilation of rewriting and strategies.
- Properties of confluence, termination, modularity.
- Theorem proving.
- Automated deduction with constraints.
- Proofs by induction.
- Observational proofs.
- Proofs of program properties.
International and industrial relations
- Participation in the Esprit project Basic Research CCL and Working Group CoFI, in the Compulog network of excellence, and in ERCIM Working groups.
- Cooperation via NSF with the university of Illinois at Urbana-Champaign (USA).
- Collaboration with research centers: the Max Planck Institut fur
Informatik (MPI), DFKI, CWI, SRI International and with universities:
Aarhus, Amsterdam, Kaiserslautern, Porto, Saarbrucken, Taiwan.
- Contracts with Cnet and GIHP Champagne.