The TERMINATOR research project is focused on the development of automatic methods for
proving program termination and general liveness properties.
The current version of TERMINATOR is
an automatic interprocedural,
path-sensitive and context-sensitive termination prover that supports
concurrent programs with
arbitrarily nested loops and recursive functions, pointers and
side-effects, and function-pointers, etc. It has been successfully used
on Windows device drivers of up to 35,000 lines of code.
The ultimate goal of the TERMINATOR project is develop
automatic techniques (and tools that implement them)
that will allow us to prove that industrial software components cannot hang.
This goal compliments today's plethora of tools that only
support the automatic
checking of safety properties for imperative software (e.g.
TERMINATOR's home is at the Microsoft Research laboratory at
Cambridge University, but many of the
come from other institutions,
Queen Mary. Several
members of the group
Several members are also involved in
SLAyer and the
The TERMINATOR project was initially formed
in 2004 during
at the Beyond Safety Retreat
at Schloss Ringberg.
The TERMINATOR group meets regularly at
Le Rostand/Jardin du Luxembourg in Paris, the Microsoft laboratory in
Cambridge, or cafes in Germany.
For more history regarding the project, read the
article entitled Terminator Tackles an Impossible Task.