Position available for O'Caml programmer in Microsoft's TERMINATOR project

["Byron Cook" <bycook@microsoft.com>]

Research Software Development Engineer: TERMINATOR project

Project website: http://www.research.microsoft.com/terminator
Site location: Microsoft Research in Cambridge, UK
Contract length: 6 months to start, with negotiation to extend
Who to contact: Byron Cook (bycook@microsoft.com)

TERMINATOR is a program termination prover that supports C programs with
arbitrarily nested loops or recursive functions, and imperative features
such as references, functions with side-effects, and function pointers.
TERMINATOR uses a newly discovered method of counterexample-guided
abstraction refinement for program termination proofs.  The termination
argument is constructed incrementally, based on failed proof attempts.
TERMINATOR also infers and proves required program invariants on demand.
It has been successfully used on Windows device drivers of up to 35,000
lines of code.

The TERMINATOR team is looking for someone with functional programming
and formal verification experience to develop and maintain the
TERMINATOR code-base.  Candidates should have the following
qualifications:
1) MS. or Ph.D. in Computer Science
2) Experience with ML or an ML-like programming language (TERMINATOR is
written primarily in O'Caml, with some C++ and Prolog)
3) Knowledge of algorithms and techniques from automatic formal
verification and compilers
4) Good communication and inter-personal skills
5) Leadership and cross-team collaboration skills
6) 2 years of industrial experience (preferred)

This position will include the following activities: Fixing bugs in the
TERMINATOR code base; providing new features in TERMINATOR; responding
to customer feature requests; improving the performance of TERMINATOR,
and improving the reliability of TERMINATOR.

This is an important position.  TERMINATOR is the first known automatic
termination prover to support real programs, and solves a problem that
is important to reactive systems (i.e. proving that they actually will
be able to react).  It has the potential to make a huge contribution to
how future developers write programs and the quality of the software
that we use.

Interested? Send a CV to Byron Cook (bycook@microsoft.com)