Paper TestCov: Robust Test-Suite Execution and Coverage Measurement accepted for presentation at ASE 2019!

Prof. Dr. Gidon Ernst

Picture of Prof. Dr. Gidon Ernst

Software and Computational Systems Lab
Institute for Informatics
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)

Room F 007, Oettingenstr. 67
Office hours
Do/Fr, by appointment
+49 (89) 2180-9376


Please send me encrypted mails!
My GPG key: 0x43E74A64
Fingerprint: 2936 1F81 7F7E 77FC 114F E87D 864B 9E41 43E7 4A64

Consider using the keyserver at


CV, Publications, Google Scholar, DBLP, ORCID, Github, Twitter


Teaching (Current Term)


My research focuses in scalable methods for software specification, testing, and verification. I am specifically interested in system properties that go beyond sequential functional correctness, such as crash tolerance for file systems, concurrency, or information flow security. I have a strong interest in tool building and applying these to realistic and practical challenges.

Concurrent Information Flow

Security Concurrent Separation Logic (SecCSL) combines reasoning about expressive, value-dependent security classifications with concurrency and low-level code.
The approach is implemented in the tool SecC (code on bitbucket).

Joint work with Toby Murray (University of Melbourne).


Falsification of temporal logic requirements for hybrid systems. See FalStar and the ARCH competition on falsification.

Joint work with Ichiro Hasuo, Sean Sedwards, Zhenya Zhang (NII Tokyo, University of Waterloo).

Theorem Proving

KIV: interactive theorem prover and software verification platform (see also VerifyThis)

Joint work with Wolfgang Reif, Gerhard Schellhorn, and others at the Institute for Software & Systems Engineering (Augsburg University).

Previous Projects

PhD Students


  • SecC: verified information flow for C.
  • FalStar: hybrid systems falsification.
  • KIV: interactive verification system.