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. BLAST, SLAM, SatAbs, etc)

TERMINATOR's home is at the Microsoft Research laboratory at Cambridge University, but many of the group's members come from other institutions, including TUM and Queen Mary. Several members of the group are SLAM-veterans. Several members are also involved in SLAyer and the East London Massive.

The TERMINATOR project was initially formed in 2004 during evening discussions 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.