++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Radboud University Nijmegen - Institute for Computing and Information Science One 3 year post-doc position in the NWO-sponsored project ARPA: Advancing the Real use of Proof Assistants ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ We are seeking one researcher at the level of Postdoc for a period of three years, starting from September 1 2006 Candidates should have - Good knowledge of at least one and preferably more of the following fields: Hybrid Systems, Formal Methods, Proof Assistants and Automated Reasoning. - A finished PhD in computer science, mathematics or logic Description of the project -------------------------- Proof Assistants help the user in developing a theory (stating definitions and lemmas), modeling systems (describing constructions, giving definitions) and verifying properties about these systems (giving proofs). So, Proof Assistants are very generic tools to support Formal Methods. Their genericity makes them less efficient than tools that are especially geared towards a specific formal method. On the other hand they have a very precise semantics, which makes a the certainty of a result that is verified by a Proof Assistant very high. This is especially the case for PAs that are able to produce "proof objects" that can be checked independently. In the future, the very high level of certainty will prevail. In this project we want to advance the use of PAs in several ways: (1) by developing a "mathematical input mode" for PAs, making theme more easy to use, (2) integration of different PAs, allowing the exchange of results, (3) developing a certified library for real number computation in Coq, (4) verifying hybrid systems in Coq, using the library of (3) to model and verify system properties. The quality of (3) will be judged by its applicability to (4), but (2) and (3) will also be judged by its applicability to the formalisation of the proof of Kepler's conjecture. For detailed information see the full project proposal. It will be sent to you on request (email to herman@cs.ru.nl). The project leader is Dr. J.H. Geuvers. The research will be performed within the research groups "Foundations" and "Informatics for Technical Applications" of the ICIS institute of the Radboud University Nijmegen, in collaboration with Prof.dr. F. Vaandrager (head of the ITA research group). The research of the post-doc will be on topics (4) above. Applications ------------ The full project proposal will be sent to you on request (herman@cs.ru.nl). Further enquiries can be made with the project leader. You are invited to send your application by email to the project leader. Deadline for applications is June 25, 2006. In case you learn of this job opportunity later than that date you may send an email to enquire whether it still makes sense to apply. Your application should consist of: - a curriculum vitae (containing information regarding your academic degrees, title of your PhD-thesis, publications) - the names and addresses of two referees