We are concerned with developing new theories, technologies, and tools for the formal verification of computer systems, including software, hardware and embedded systems.

The main research directions of our group are:

• Software verification, with particular focus on model checking, runtime verification, deductive software verification, and verification-based testing;
• Automated reasoning, with particular focus on decision procedures, first-order theorem proving, inductive theorem proving, and theory exploration;
• Contract verification, with particular focus on specification and analysis of contracts.

Current projects

Software tools

• Aligator: Invariant Generation by Algebraic Techniques
• Vampire: Automatic first-order theorem prover

Previous projects

HATS
	Highly Adaptable and Trustworthy Software using Formal Methods, an Integrated Project supported by the 7th Framework Programme of the EC within the FET. In HATS we develop a methodological and tool framework to achieve not merely far-reaching automation in maintaining dynamically evolving software, but an unprecedented level of trust while informal processes are replaced with rigorous analyses based on formal semantics.
CHARTER
	CHARTER aims at easing, accelerate, and cost-reduce the certification of critical embedded systems by melding realtime Java Model Driven Development, rule based compilation, and formal verification.
The KeY project
	We have developed the KeY tool, which is a commercial tool for object-oriented software development augmented with a prover. The KeY allows users to develop guaranteed correct Java Card programs.
COST IC0701
	COST Action IC0701 is a European scientific cooperation. The Action aims to develop verification technology with the reach and power to assure dependability of object-oriented programs on industrial scale.
COST IC0901
	COST Action IC0901 is a European scientific cooperation. The main objective is making automated reasoning techniques and tools applicable to a wider range of problems, as well as making them easier to use by researchers, software developers, hardware designers, and information system users and developers.
MiniSat
	MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT. It is released under the MIT licence, and is currently used in a number of projects.
Mobius
	Mobility, Ubiquity and Security, an Integrated Project launched under the FET Global Computing Proactive Initiative and supported by the European Commission through the 6th Framework program.
Cedes
	Cost efficient dependable electronic systems, a project within IVSS (Intelligent Vehicle Safety Systems) research programme.