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, ORCID, Github, Twitter

This Page

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

Informationen zu Prüfungen/Klausuren

Folgende Prüfungen werden als Präsenzklausuren stattfinden:

Formale Spezifikation und Verifikation SoSe 2020 Hauptklausur:
05.08.2020, 14-16 Uhr
Softwaretechnik WS 2019/20 Nachklausur:
14.08.2020, 10-12 Uhr
Informatik Einführung für Nebenfach WS 2019/20 Nachklausur:
23.09.2020, 14-18 Uhr

TeilnehmerInnen erhalten im Vorab nochmals eine E-Mail mit allen wichtigen Informationen bezüglich den Hygienemaßnahmen. Bitte lesen Sie diese Informationen aufmerksam durch.

Das Prüfungsamt bittet darum, dort keine Anfragen zu Klausurterminen zu stellen.
Falls Sie ein konkretes Anliegen haben, kontaktieren Sie mich bitte direkt per E-Mail.

Wichtige Hinweise

Tragen Sie in den Gebäuden der Universität immer einen Mund-Nase-Schutz.
Sie sind grundsätzlich selbst für die Beschaffung eines solchen verantwortlich.
(Wir haben einige wenige Ersatzmasken vorrätig)
Die Teilnahme an Präsenzveranstaltungen ohne Mund-Nase-Schutz,
mit klaren/anhaltenden Krankheitssymptomen oder mit einer akuten Infektion ist nicht zulässig.
Für alle unsere Präsenzveranstaltungen wurde eine Gefahrenbeurteilung durchgeführt
und ein Hygienekonzept erstellt. Über beides werden Sie zeitnah informiert.
Hygienebestimmungen der Universität Bayern e.V.
Ergänzenden Regelungen der LMU
Wir bitten Sie, die Corona-App zu verwenden
Darüber hinaus gelten natürlich alle vorbeugenden Maßnahmen (Handhygiene, Mindestabstand von 1.5m)

Eine Liste aller Prüfungstermine die bereits feststehen finden Sie hier.

Recent

Paper accepted: Dongge Liu, Gidon Ernst, Toby Murray, Ben Rubinstein: Legion: Best-First Concolic Testing. ASE 2020. See also the competition on software testing.
Falsification Competition: I am organizing the friendly competition on falsification at the ARCH workshop! Let me know until end of April if you are interested.
Corona-Update: Das Sommersemester 2020 findet wegen der Schließung der LMU-Gebäude bis auf Weiteres komplett online statt. Alle Prüfungen sind bis auf das Ende des Semesters verschoben (das gilt auch für Nachprüfungen aus dem Wintersemester).
Test-Comp 2020: Results are available. Our tool Legion did well in many categories! With Dongge Liu, Ben Rubinstein, Toby Murray (University of Melbourne).
Gastvorträge am 27.11.: Prof. Dr. Ralf Ludwig, Andrea Böhnisch, Magdalena Mittermeier Klimawandel und Extremereignisse – neue Erkenntnisse für die Klimafolgenforschung durch die Nutzung von HPC.
Vielen herzlichen Dank an Students for Future Munich.
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.
VerifyThis 2020: Long-term challenge and my contribution (github, ongoing) to use formal methods to analyze the design and implementation of a PGP keyserver.
The challenge is open to any approach and tool, programming and specification language; at a scope of your choice (abstract models, code verification, functional vs security properties).
See also HAGRID (the reference implementation hosting https://keys.openpgp.org/).
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.
Tool: SecC: A verifier for C that supports expressive information flow and concurrency.

Teaching (Current Term)

Wintersemester 2020/21

Einführung in die Informatik: Programmierung und Softwareentwicklung für Nebenfach (Ernst, Wendler, 3+1+2)
Masterseminar "Software Quality Assurance" (Ernst, Kanav, in English, 2)

Sommersemester 2020

Thesis Mentoring (see also)

Available topics

LTL specifications in deductive verification

Development of an interactive theorem prover for untyped logic

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

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

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

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

oint 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

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

Cuvée: SMT-LIB with Programs and Weakest Preconditions (new).
Arse: LL parsing for Scala case classes made simple (new).
SecC: verified information flow for C.
FalStar: hybrid systems falsification.
KIV: interactive verification system.

Service

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