PROTHEO : Constraints, automatic deduction and software properties proofs (project-team)

About the project : Project-Team site Activity report Videos and photos Research reports Theses Theme : Sym Symbolic systems Nancy - Grand Est research center

PROTHEO has been dissolved on 12/31/2007

Project-Team Presentation

LORIA joint project-team with CNRS, University Henri Poincaré, University Nancy 2 and INPL.

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.

Research themes

• 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.

The team develops several software packages, including Spike (a software for studying induction-based reasoning and first-order proofs), Elan (a logical framework for prototyping constraint resolution tools and deduction processes) and daTac (a first-order theorem prover in associative commutative theories).

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.

Scientific leader

Claude KIRCHNER
+33 3 54 95 84 05
Claude.Kirchner@inria.fr
Secretary : +33 3 54 95 84 02