We investigate tools that automatically analyze and verify properties of
systems (at all levels of the software development process,
i.e.,whether the system is only a requirement specification, already a
design model or even a piece of program code). The tools are
semantics-based. This means that they manipulate their input on an
abstract level, in the same way that we abstract a mathematical object
by its meaning in a mathematical theory (e.g., a fraction by a rational
number). The tools delegate part of their work to dedicated modules
(constraint solvers, decision procedures, theorem provers) that account
for the mathematical theories for data and control constructs.

A part of the difficulty (and attractiveness) of our research activity
is that we must (and can) first define the mathematical theory for the
input to our tools, and define the analysis and verification problem as
an algorithmic problem (which is when the fun part starts).