The ProVal team was stopped at the end of August 2012, and reborn into a new team
Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.
Software
Program Verification
- Why3: A multi-input multi-prover verification platform
- Why (version 2): the former version of Why (includes Krakatoa and the Jessie plug-in of Frama-C)
- Frama-C: Environment for Static Analysis of C source, developed in collaboration with CEA-List and now mainly maintained by CEA
Automated Deduction
- Alt-Ergo: automatic prover modulo theories
- CiME: term rewriting toolbox
- Cubicle: a Parallel SMT-based model checker for parameterized systems
- Gappa is a tool for automatically verifying properties on numerical programs dealing with floating-point or fixed-point arithmetic. While it is intended to be used directly, it can also act as a backend prover for the Why platform or as an automatic tactic for the Coq proof assistant.
Synchronous Programming
- Reactive ML: Synchronous reactive programming in Objective Caml
- Lucid Synchrone: experimental language for the implementation of reactive systems
Data Centric Languages
- CDuce: an XML-oriented functional language
Objective Caml libraries and tools
- bibtex2html: generation of HTML pages from bibliographies
- Ocamlgraph: Objective Caml library for graphs
- Mlpost: Ocaml front-end for producing figures
Coq Libraries
- Coccinelle: a Coq library for term rewriting systems
- ALEA: a Coq library for reasoning on randomized algorithms
- PFF: a Coq library on floating-point arithmetic
- Flocq (Floats for Coq) is a formalization of floating-point arithmetic for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic; it also supports efficient numerical computations inside Coq.
- Coq.Interval provides a Coq tactic for automatically proving some inequalities between real-valued expressions containing elementary functions.