[isabelle] Postdoc and PhD Studentship: Automatic Proof Procedures with Engineering Applications
- To: dreamers at inf.ed.ac.uk, lfcs-interest at dcs.ed.ac.uk, stp at macs.hw.ac.uk, spls at mailhost.dcs.gla.ac.uk, sicsa-modabs at inf.ed.ac.uk, sicsa-cse at list-serve.hw.ac.uk, isabelle-users <isabelle-users at cl.cam.ac.uk>, pvs at csl.sri.com, proofpower at lemma-one.com, coq-club at inria.fr, types-list at lists.seas.upenn.edu, twelf-list at itu.dk, metaprl-users at metaprl.org, mizar-forum at mizar.uwb.edu.pl, types at lists.chalmers.se, theorem-provers at ai.mit.edu, elsnet-list at let.uu.nl, fmcad at utlists.utexas.edu, w3c-math-wg at w3.org, zforum at prg.ox.ac.uk, FMnet at jiscmail.ac.uk, procos at jiscmail.ac.uk, ki-inf at uni-koblenz.de, kr at kr.org, lics at informatik.hu-berlin.de, lics at research.bell-labs.com, math.logik at gmx.net, haskell at haskell.org, theory-logic at CS.CMU.EDU
- Subject: [isabelle] Postdoc and PhD Studentship: Automatic Proof Procedures with Engineering Applications
- From: Lawrence Paulson <lp15 at cam.ac.uk>
- Date: Fri, 15 Oct 2010 10:53:29 +0100
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.
Applications for both positions are due by Monday 15th November 2010.
We expect both post-holders to start before 1st May 2011, preferably
For additional information on the project and the positions, please
visit our project website
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and