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

Team presentation

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.

Keywords: Formal specification Software verification Automated deduction Mechanized reasoning Constraint solving Term rewriting

Inria Headquarters and research centres

Direct links

Social