• Automated Theorem Proving and its applications is an important activity of the team. It includes research on satisfiability modulo theories (Alt-Ergo prover), numerical constraint solving (Gappa solver), and applications such as SMT-based model-checking (Cubicle tool). Furthermore, the group also engages in the evolution of interactive theorem proving systems (Coq and Isabelle).
  • The verified computer arithmetic consists of proving programs that contain computations involving floating-point numbers, which are primarily used as an efficient way of approximating real numbers. We develop formalizations of floating-point arithmetic and automated tools for obtaining intricate results about the inaccuracies introduced by floating-point computations, taking into account peculiarities of architectures and compilers. Applications include numerical analysis programs.
  • Formalizing in a broad sense is an activity involving all members, in particular using assistants like Coq and Isabelle. We formalize the semantics of specification and programming languages, including concurrency, probability, time, mathematical/numerical operations, etc... This activity is inherently fundamental for all deductive and testing-based verification activities.
  • We are interested in the design and development of programming languages and systems that seriously take into account massive data. This includes improving existing languages and systems. Ultimately, we aim at providing formally verified implementations of data intensive management systems.
  • Testing is also a strong research activity of the team. Important directions include scaling up testing techniques by handling efficiently the concurrency aspects of distributed systems (for instance Web services, wireless self-organised networks, etc.) as well as by advancing symbolic and probabilistic approaches. Moreover, we try to overcome the infeasible paths issues for the test of C programs by finding suitable combinations with static analysis methods.
  • Our approach to deductive program verification is in need for improved techniques for modular reasoning, support for genericity, for higher-order programs, for refinement-based approaches. These features are essential for scaling-up, in particular via the development of reusable verified libraries.