PhD position on the verification of automated reasoning using Isabelle

Prof. Christoph Weidenbach, Dr. Jasmin Blanchette, Dr. Sophie Tourret, Max-Planck-Institute for Informatics, Saarbrücken, Germany

The Automation of Logic group is looking for a PhD student to work on the formal verification of the metatheory of automated reasoning using the Isabelle proof assistant.

Researchers in automated reasoning spend a substantial portion of their work time developing proof calculi (e.g., variants of DPLL, resolution, superposition) and proving metatheorems about them. These proofs are typically carried out with pen and paper, which is error-prone and often tedious. As part of the IsaFoL (Isabelle Formalization of Logic) project, we are interested in formalizing results concerning existing logical calculi. The motivation is manifold:

The exact nature of the PhD project will be determined together with the candidate. Two potential projects are the following:

The candidate should ideally have some experience with automated or interactive theorem proving, or with some closely related area of theoretical computer science (e.g., term rewriting). To apply, please send your personal record (including CV, grade transcripts, and contact information for two references) by email to Jennifer Müller. The start date is negotiable.