[isabelle] PhD position in Computational Logic at the University of Innsbruck

PhD position in Computational Logic at the University of Innsbruck

The research group computational logic headed by Prof. Aart Middeldorp
at the university of Innsbruck has an open position for a PhD student
which is funded by the FWF (Austrian science fund) via the project
"Improving Certifiers for Termination Proofs".

The project aims at increasing the reliability in current termination
provers by independently checking the generated proofs. To this end,
several termination techniques will be developed in the theorem prover
Isabelle/HOL, in combination with executable functions which check
for the correct application of these techniques.

For this project, we are looking for an enthusiastic young researcher
with a background in formal methods. Knowledge of term rewriting and
theorem proving would be an asset. Candidates with a strong theoretical
background in related areas are also encouraged to apply. The ideal
candidate furthermore enjoys the opportunity of working with students
at all levels. The candidate must have a Master's or equivalent degree
(Diplom). Knowledge of German is an advantage but not essential.

The preferred starting date is Oktober 1, 2010.

The annual gross salary of the position (30 hours research per week)
is approximately EUR 25,915, where additional salary can be gained
via teaching.

Applications (including CV) may be mailed to the project leader
René Thiemann no later than September 12, 2010, preferably by email:

Dr. René Thiemann
Institute of Computer Science
University of Innsbruck
Techniker Str. 21a
A-6020 Innsbruck
Email: rene.thiemann at uibk.ac.at

Informal inquiries are also welcome via email.

The city of Innsbruck, which hosted the Olympic Winter Games in 1964 and
1976, is superbly located in the beautiful surroundings of the Tyrolean
Alps. The combination of the Alpine environment and urban life in this
historic town provides a high quality of living. The University of
Innsbruck has a long tradition dating back to the 16th century and offers
a wide spectrum of research and teaching activities with interesting
opportunities for interdisciplinary collaboration.

Further information is available from the following links:

Existing Formalization of Termination Techniques:
Computational Logic Research Group:
Institute of Computer Science:
University of Innsbruck:
City of Innsbruck:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.