Prof. Dr. Gidon Ernst, LMU Munich

Prof. Dr. Gidon Ernst

Junior Professor, Software Verification

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

Office: Room F 007, Oettingenstr. 67
Office hours: By appointment, via https://meet.lrz.de/gidon
Phone: +49 (89) 2180-9376
E-Mail: firstname.lastname@lmu.de

GPG-Key

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 https://keys.openpgp.org/.

Personal

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

This Page

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

Recent

Publication: Dongge Liu, Gidon Ernst, Toby Murray, Ben Rubinstein: Legion: Best-First Concolic Testing. ASE 2020, Preprint. See also the competition on software testing.
Publication: Proceedings of the ARCH workshop 2020, including the report of the falsification competition.
Publication: Proceedings of the VerifyThis long-term challenge, including a testing approach (with Lukas Rieger), and an approach to verifying the information flow (with Toby Murray).
Talk at the CPAchecker workshop 2019 on VerifyThis challenges in sv-benchmarks. Slides, SV-COMP 2020.
Talk at the Alpine Verification Meeting 2019 on Security Concurrent Separation Logic. Slides, Project.
Publication: Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo: Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input. QEST 2019. Draft.
Publication: Gidon Ernst and Toby Murray: SecCSL: Security Concurrent Separation Logic. CAV 2019. Draft, Slides, Project.
Invited Talk in the Ringvorlesung of the Software Engineering Elite Graduate Program of Uni Augsburg, LMU, TUM: SecCSL: Security Concurrent Separation Logic. Slides (in german), Project.
Invited Talk at TYPES in Munich 2019: Applications of type theory for software verification. Slides.

Lehrveranstaltungen (siehe auch)

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

Einführung in die Informatik: Programmierung und Softwareentwicklung für Nebenfach (Ernst, Wendler, 3+1+2)
Vorlesung: via Aufzeichnung/Folien, Übung: teilweise in Präsenz geplant.
Formale Spezifikation und Verifikation (Ernst, Holzner, 3+2)
Vorlesung: via Aufzeichnung/Folien, Übung: teilweise in Präsenz geplant.
Masterseminar "Software Quality Assurance" (Ernst, Kanav, in English, 2)
Supervision: remotely, presentations: online live or as video recordings

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)

Guided fuzz testing with stochastic optimization

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

Further topics can be discussed on request.

Research

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

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

KIV: interactive theorem prover and software verification platform (see also VerifyThis)
Flashix: verified file system for flash memory (github)
With Wolfgang Reif, Gerhard Schellhorn, Jörg Pfähler, Stefan Bodenmüller (Augsburg University).
IMP3: integration of shape analysis and theorem proving
Takatuka: Java Virtual Machine for sensor networks

PhD Students

Dongge Liu: Software fuzzing with machine learning (2018–).
Co-supervised with Ben Rubinstein, Toby Murray (University of Melbourne).

Software

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.

Service

PC co-chair: FTfJP 2019 at ECOOP 2019
Co-organizer: AVM 2020 (postponed to 2021), ARCH 2020, ARCH 2019, VerifyThis 2018
PC: HSCC 2021, VSTTE 2020, SAC 2020, 4PAD 2019, SAC 2019, 4PAD 2018
PC (artifact evaluation): HSCC 2020, SAS 2018