[isabelle] Job offer on formalizing complexity and termin... · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Job offer on formalizing complexity and termin...

Email Gateway (Aug 19 2022 at 16:29):

From: René Thiemann <rene.thiemann@uibk.ac.at>
[Apologies for cross-posting]

2-year postdoc or 3-year PhD-student position at the University of Innsbruck
============================================================================

The Computational Logic research group at the University of Innsbruck has one
open position funded by the FWF (Austrian science fund) via the START project
„Certifying Termination and Complexity Proofs of Programs“.

The project aims at increasing the reliability in current complexity and
termination provers by independently checking the generated proofs. To this end,
several analysis techniques will be formalized 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 computational logic. Knowledge of automated termination analysis,
complexity analysis, or theorem proving would be an asset. Candidates with a
strong theoretical background in related areas are also encouraged to apply.
The PhD-student candidate must have a Master's or equivalent degree. Knowledge
of German is an advantage but not essential.

The preferred starting date is within the first quarter of 2015.

The salary is determined by the FWF-funding scheme (3.483,40 EUR monthly
gross salary for postdocs, and 1.996,90 EUR for PhD-students, cf.
http://www.fwf.ac.at/en/research-funding/personnel-costs/)

Applications (including a CV, a publication list (only for postdocs), and a
letter of recommendation) may be emailed to the project leader René Thiemann
(rene.thiemann at uibk.ac.at) no later than December 14, 2014.

Informal inquiries are also welcome via email.

The city of Innsbruck 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.

Further information is available from the following links:

START Project:
http://cl-informatik.uibk.ac.at/research/projects/certifying-termination-and-complexity-proofs-of-pr/

Institute of Computer Science:
http://informatik.uibk.ac.at/

University of Innsbruck:
http://www.uibk.ac.at/

City of Innsbruck:
http://www.innsbruck.at/

Email Gateway (Aug 22 2022 at 16:27):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
3-year postdoc and 3-year PhD-student position at the University of Innsbruck
============================================================================

The Computational Logic research group at the University of Innsbruck has two
open positions funded by the FWF (Austrian science fund) via the START project
„Certifying Termination and Complexity Proofs of Programs“.

The project aims at increasing the reliability in current complexity and
termination provers by independently checking the generated proofs. To this end,
several analysis techniques will be formalized in the theorem prover
Isabelle/HOL, with a focus on LLVM and integer transition systems.

For this project, we are looking for two enthusiastic researchers with a
background in computational logic. Knowledge of automated termination analysis,
complexity analysis, or theorem proving would be an asset. Candidates with a
strong theoretical background in related areas are also encouraged to apply.
The PhD-student candidate must have a Master's or equivalent degree. Knowledge
of German is not essential.

The salary is determined by the FWF-funding scheme (3,627 EUR monthly
gross salary for postdocs, and 2,071 EUR for PhD-students, cf.
http://www.fwf.ac.at/en/research-funding/personnel-costs/)

We plan to make decisions on these positions in December 2017.

The preferred starting date is within the first three months of 2018.