Paper accepted at TACAS'21: "Bridging Arrays and ADTs in Recursive Proofs"

Prof. Dr. Gidon Ernst

Junior Professor, Software Verification

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
By appointment, via
+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, Github, Twitter

Interests: formal methods for software engineering, software testing, interactive and automated proofs, hybrid systems falsification.

This Page

Recent, Teaching, Thesis Mentoring, Research, Software, Service


Lehrveranstaltungen (siehe auch)

Sommersemester 2021 (Vorlesungszeitraum: 12.4.-16.7.)

  • Advanced Topics in Software Engineering (Mastervorlesung)
  • Seminar "Software Quality Assurannce" für Studierende im Bachelor und Master

Wintersemester 2020/21 (Vorlesungszeitraum: 2.11.-12.2.)

Organisatorische Details werden auf Uni2Work bekanntgegeben sobald diese feststehen.

Thesis Mentoring (see also)

Currently assigned topics
Information flow testing for PGP keyservers
Implement Fuzzing in CPAchecker
SMT-based checking and synthesis of formal refinements
Frontends for a deductive verifier (Python)
Frontends for a deductive verifier (Boogie)
Interactive verification debugging
Simplification and solving strategies for SMT
Development of an interactive theorem prover for untyped logic
Finished topics
Specifying Loops with Contracts. [1]
Rely/Guarantee Reasoning for Separation Logic in SecC
Loop Contracts for Boogie and Dafny
Guided fuzz testing with stochastic optimization
Further topics can be discussed on request. Before contacting me with your own topic proposal, please think about this first: What would be the scientific question leading your project? Does the topic fit well with the research and teaching area of Prof. Ernst?


Softare Testing

Legion is a software tester based on a tight integration of concolic execution and fuzzing, mediated by Monte-Carlo tree search. Input values to target a specific part of the program are generated by approximate path-preserving fuzzing, a variant of constrained random sampling, using an adaption of the Quicksampler algorithm.

Joint work with Dongge Liu, Ben Rubinstein, Toby Murray.

See also the competition on software testing.

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).

Previous Projects

PhD Students


  • Korn: Horn-clause based verifier for C, draft.
  • Legion: tight integration of concolic execution and fuzzing.
  • Cuvée: SMT-LIB with programs and weakest preconditions, draft.
  • Arse: LL parsing for Scala case classes made simple.
  • SecC: verified information flow for C.
  • FalStar: hybrid systems falsification.