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