---------- Forwarded message ---------- From: Lawrence Paulson <[email protected]>
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. _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
