The Coq mailing list

[Lawrence Paulson <lp15 AT cam.ac.uk>]

AUTOMATIC PROOF PROCEDURES FOR POLYNOMIALS AND SPECIAL FUNCTIONS

A Postdoc and PhD Studentship are available on our EPSRC-funded
Cambridge/Edinburgh project, which concerns scalable proof procedures
for real arithmetic involving polynomials and special functions
(transcendental, hyperbolic, etc.). The project will create new
verification techniques for hybrid and control systems by developing
powerful arithmetic proof procedures targeted to classes of problems
arising in engineering practice. Our approach combines intensive work
on the procedures themselves with careful study of application areas
in collaboration with specialists.

Specifically, we have available

* a 4 year Postdoctoral Research Associate position (Automated Reasoning 
  Group, Computer Laboratory, University of Cambridge), and

* a 3.5 year PhD studentship (Laboratory for Foundations of Computer 
  Science, School of Informatics, University of Edinburgh).

The PhD student and postdoc will join an energetic and highly
collaborative team of two Principal Investigators

- Prof. Lawrence C. Paulson  http://www.cl.cam.ac.uk/~lp15/
- Dr. Paul B. Jackson        http://homepages.inf.ed.ac.uk/pbj/

one additional postdoc 

- Grant Olney Passmore   http://homepages.inf.ed.ac.uk/s0793114/

and an already-appointed PhD student.  Visits between the two sites
will be encouraged.

REQUIREMENTS FOR THE POST-DOCTORAL RESEARCH ASSOCIATE 

We are especially interested in the process of transforming an
engineering problem (perhaps expressed by differential equations) into
a form acceptable to our tools (inequalities involving special
functions), and further transforming the problem to make it easier to
solve. This process then needs to be automated using computer algebra
techniques. Another important task is further development of the
theorem proving technology itself. The applicant should therefore have
strong software development skills and either a firm knowledge of
engineering mathematics or a background in automated theorem proving.

REQUIREMENT FOR PHD STUDENTSHIP

The applicant should have a strong grounding in logical and
mathematical aspects of computer science, with a keen interest in
developing and applying software tools for the formal verification of
real-world engineering artefacts.

FURTHER DETAILS

Applications for both positions are due by Monday 15th November 2010.

We expect both post-holders to start before 1st May 2011, preferably
sooner.

For additional information on the project and the positions, please
visit our project website

 http://www.cl.cam.ac.uk/~lp15/Grants/AutoPolyFun/. ;

Follow the links on the right-hand side of the page for specific
information on how to apply for either for these positions.

-- 

The University of Cambridge values diversity and is committed to
equality of opportunity.

The University of Cambridge has a responsibility to ensure that all
employees are eligible to live and work in the UK.

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.