Three students accepted for Google Summer of Code at SoSy-Lab

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
Mi-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


Curriculum vitae, Google Scholar, DBLP, ORCID, Github, Twitter



  • Paper accepted: Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo: Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input. To appear at QEST 2019. Draft.
  • Invited Talk at TYPES in Munich 2019: Applications of type theory for software verification. Slides.
  • Paper accepted: Gidon Ernst and Toby Murray: SecCSL: Security Concurrent Separation Logic. To appear at CAV 2019. Draft.
  • Tool: SecC: A verifier for C that supports expressive information flow and concurrency.


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.


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.

Joint work with Toby Murray


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.

Previous Projects