The Department of Computer Science at the Faculty of Engineering and Natural Sciences at Johannes Kepler University Linz invites applications for a permanent full-time position at the Institute for Formal Models and Verification (FMV) founded by Armin Biere.

We are looking for candidates who work in fields like

  • Formal verification or synthesis of software and hardware
  • Techniques and tools of formal verification (e.g., model checking, equivalence checking, deductive verification, symbolic execution)
  • Formal models and languages (e.g., logic-based languages, graph transformation systems, Petri nets, process algebra)
  • Automatic reasoning and decision procedures (e.g., SAT, SMT, first-order logic, interactive theorem proving)
  • Theoretical foundations of formal verification or synthesis (e.g., computational logic, complexity theory, discrete structures, game theory)
  • Applications of verification and synthesis like concurrent/distributed systems, cyber-physical systems, analysis of programs and protocols, biological applications, and future technologies like quantum computing and artificial intelligence
  • Model-based testing and runtime verification
  • Formal analysis and verification of artificial intelligence technologies
  • Probabilistic and statistical approaches for formal reasoning

Informal enquiries are welcome and may be sent to