Terminator Research Project

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 EPFL, MPI-Saarbrücken, 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 regularily at Le Rostand/Jardin du Luxembourg in Paris, the Microsoft laboratory in Cambridge, or MPI in Saarbrücken. For more history regarding the project, read the article entitled Terminator Tackles an Impossible Task.

We've posted a draft of a new paper, entitled CFL-Termination, that describes a new method of proving recursive programs terminating.
Our paper, entitled Proving that non-blocking algorithms don't block, will appear at POPL'09.
Rick Rashid (Senior VP of Microsoft Research) discusses TERMINATOR, termination, and liveness in his TechFest keynote address. See the video (at 29m into the talk).
Byron will be giving a set of lectures on termination at the Marktoberdorf summer school and Trends in Concurrency summer school.
Watch a recent video interview about TERMINATOR from channel9.msdn.com. Also: here is a second interview which goes into more detail about TERMINATOR's internals.