2 Papers accepted at SEFM'20: "Difference Verification with Conditions" and "FRed: Conditional Model Checking via Reducers and Folders"

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)

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

Teaching (Current Term)

Wintersemester 2020/21

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

PhD Students

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