Position on Formal Modeling and Tool-Supported Verification (Ph.D./Postdoc/Senior Researcher)


Faithful formal models and tool-supported reliable verification are essential for establishing reliable guarantees for program analyses and, more generally, for IT systems. The development of complex analyses and IT systems is known to be error prone. Hence, formal methods should be applied in critical domains where bugs cannot be tolerated.

Formal modeling languages provide the basis for precisely specifying the behavior of an IT system at some layer of abstraction, the requirements that a system should satisfy, and the properties that a system does satisfy. Formal modeling languages can also be employed for specifying the semantics of programming / byte-code / machine languages, for specifying static / dynamic program analysis techniques at a conceptual level, and for specifying relationships between multiple specifications (e.g. that one specification constitutes a refinement of another specification or that a system specification satisfies a requirement specification). Formal verification techniques provide the basis for verifying properties of specifications and relationships between specifications with mathematical rigor.

Tool support is crucial for ensuring the correctness of a formal verification and for simplifying the verification process by providing a high degree of automation. Tools like Isabelle/HOL or Coq support higher-order concepts (i.e., quantification over functions and relations), and this expressiveness is helpful for modeling and verifying complex systems / properties (e.g., soundness of a static security analysis). Model checkers support less expressive logics, but have the advantage of being fully automatic.

The Position

In this position, your research will contribute to advancing formal modeling techniques, semantic-based verification techniques, and verification tools, and it shall contribute to ensuring the reliability of program analyses and program transformations using formal methods. For the latter, multiple application areas are possible that fit different backgrounds and interests. For instance, you could use and develop formal methods
  • for proving the effectiveness of run-time monitoring and enforcement and for ensuring that the effectiveness is preserved under optimizations;
  • for attacker modeling and for proving the effectiveness of countermeasures, possibly generating effective countermeasures automatically;
  • for proving the soundness of static program analyses and program transformations for information-flow security;
  • for establishing information-theoretic soundness of quantitative information-flow and side-channel analyses; or
  • for capturing the behavioral features of micro-architectural components (e.g., caches, instruction pipelines, or schedulers) to enable the development of sound side-channel analyses.
You are expected to contribute to teaching as a tutor for lectures/exercises and for lab courses.

Prior Skills and Experiences

You should
  • be competent in at least one formal modeling language, specification language, or mathematical logic;
  • be familiar with at least one formal verification tool or model checker; and
  • be interested to push forward formal methods and their application.
In addition, you should be highly motivated to tackle challenging research problems, to produce innovative insights and tools, to strive for international visibility as a researcher, and be open minded. You need good language skills in English (writing and talking). Prior knowledge of the German language is not expected, but you should be willing to obtain basic skills within a year.

Candidates for a postdoc or senior researcher position should have a publication record on formal methods.

Formal Prerequisites

What we offer

How To Apply

The Environment

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang