Topic

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.

• research problems that are interesting, challenging, and relevant
• funded positions (salary depends on experience and percentage of employment) or scholarships
• excellent technical equipment and workplace
• competent mentoring and highly motivated colleagues
• a top Computer Science department in Germany (frequently the top CS department) with excellent B.Sc./M.Sc. students

TU Darmstadt is one of Germany's top technical universities with an outstanding reputation in research and education in Computer Science. TU Darmstadt is an equal opportunities employer and encourages applications from women. In case of equal qualifications, applicants with a degree of disability of at least 50% will be given preference.

The chair MAIS is led by Prof. Dr. Heiko Mantel. The overall goal of MAIS is to increase the trustworthiness and reliability of software-based systems. The working language at the chair is English.