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

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

[Byron Cook]

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)

Re: [Caml-list] Position available for O'Caml programmer in Microsoft's TERMINATOR project

[Goulagman]

Hello,

I was just wondering why you didn't use Microsoft's F# language
instead of OCaml.
Have you planned to port it to F# or are you sticking with Ocaml? And
if so, why? (I don't know much about F#).

Alexandre ABRAHAM
William CALDWELL

RE: [Caml-list] Position available for O'Caml programmer inMicrosoft's TERMINATOR project

[Josh Berdine]

Hi,

The short answer is that we use both the OCaml and F# compilers for
Terminator.  There is an answer on the FAQ:

http://research.microsoft.com/terminator/faq.htm

Cheers,  Josh


-----Original Message-----
From: caml-list-bounces@yquem.inria.fr
[mailto:caml-list-bounces@yquem.inria.fr] On Behalf Of Goulagman
Sent: 10 February 2006 4:07 pm
To: caml-list@inria.fr
Subject: Re: [Caml-list] Position available for O'Caml programmer
inMicrosoft's TERMINATOR project

Hello,

I was just wondering why you didn't use Microsoft's F# language
instead of OCaml.
Have you planned to port it to F# or are you sticking with Ocaml? And
if so, why? (I don't know much about F#).

Alexandre ABRAHAM
William CALDWELL

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs