Research Associate: Automatic Proof Procedures with Engineering Applications

Faculty of Computer Science & Technology

Vacancy Reference No: NR07330  Salary: £27,319-£35,646

Limit of tenure applies*

We are seeking a Post-Doctoral Research Associate to join an energetic collaborative project (joint with Edinburgh University) concerned with proof procedures for real arithmetic problems 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.

The RA's role can be flexible, but 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.

The position is funded by the EPRSC grant EP/I011005/1, led by Prof. Lawrence C. Paulson, to whom enquiries should be addressed. For additional information, please visit our project website.

Start date: as soon as possible after 15 November 2010 and no later than 1 May 2010.

Applications should include:

Please send your application by e-mail to personnel-admin@cl.cam.ac.uk.

* Limit of tenure: Up to 48 months.

Closing date: Monday, 15th November, 2010.