Prof. Dr. Gidon Ernst
Junior Professor, Software Verification

Software and Computational Systems Lab
Department of Computer Science
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
- firstname.lastname@lmu.de
- Phone
- Please note that I no longer have an office phone
- Chat
- Zulip (LMU/IFI internal)
- ORCID
-
0000-0002-3289-5764
GPG-Key
Please send me encrypted mails!
My GPG key: 0x43E74A64
Fingerprint: 2936 1F81 7F7E 77FC 114F E87D 864B 9E41 43E7 4A64
Personal
CV, Google Scholar, Semantic Scholar, DBLP, ORCID, GitHub, Twitter
- formal methods for software engineering
- software testing
- interactive and automated proofs
- hybrid systems falsification
This Page
Recent, Teaching, Thesis Mentoring, Research, Software, Service
Recent
- [01/2023] Award: I have received the award “best master lecture” 2022 in computer science for my course Methods in Software Engineering by the student association Gruppe Aktiver Fachschaftika. I highly appreciate this recognition and would like to thank everybody involved, notably Nian-Ze Lee for massive help with the preparations and for an excellent tutorial.
- [11/2022] Invited Talk: Loop Verification with Invariants and Contracts at Dagstuhl Seminar Principles of Contract Languages, Slides, Tool Cuvée, Demo: inference and framing
- [10/2022] Publication: Gidon Ernst, Alexander Knapp, Toby Murray: A Hoare Logic with Regular Behavioral Specifications, ISoLa 2022, Paper, Slides, arXiv
- [01/2022] Presentation of Loop Verification with Invariants and Contracts at VMCAI 2022, Paper, Technical Report, Slides, Video
- [12/2021] Paper Accepted: Dongge Liu, Van-Thuan Pham, Gidon Ernst, Toby Murray, Benjamin Rubinstein: State Selection Algorithms and Their Impact on The Performance of Stateful Network Protocol Fuzzing, SANER 2022.
- [12/2021] Publication of the report from the falsification category category of ARCH-COMP 2021. DOI: Paper, Data; GitLab.
- [12/2021] Results for Test-Comp: This year we participated with a new implementation of Legion called Legion/SymCC. It is based on the SymCC backend and shows competitive results in many categories, despite being an early prototype.
- [12/2021] Results for SV-COMP: My tool Korn did well in some categories, notably ReachSafety-Recursive!
- [10/2021] Paper Accepted: Gidon Ernst: Loop Verification with Invariants and Contracts, VMCAI 2022, Technical Report
- [08/2021] Publication: Gidon Ernst, Johannes Blau and Toby Murray: Deductive Verification via the Debug Adapter Protocol, F-IDE 2021, DOI.
- [07/2021] Publication: Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo: Falsification of Hybrid Systems Using Adaptive Probabilistic Search, ACM TOMACS. DOI.
- [07/2021] Presentation of the results from the falsification category category of ARCH-COMP 2021.
- [04/2021] VerifyThis 2021 solution to challenge 2 in SecC: Linked List to Binary Tree
- [12/2020] Publication: Grigory Fedyukovich, Gidon Ernst: Bridging Arrays and ADTs in Recursive Proofs, TACAS 2021, DOI.
Lehrveranstaltungen (siehe auch)
Wintersemester 2022/23
- Einführung in
die Informatik: Programmierung und Softwareentwicklung für Nebenfach
(Ernst, Wendler, 3+1+2)
- Formale
Spezifikation und Verifikation (Ernst,
Baier, 3+2)
- Bachelor-Seminar: Formale Methoden für Cyber-Physical Systems (via Zentralanmeldung) (Ernst, Brieger)
Sommersemester 2022
- Lecture: Methods in
Software Engineering (in English, Bachelor and Master) (Ernst, Lee)
- Bachelor-Seminar: Programmsynthese (via Zentralanmeldung) (Ernst, Brieger)
Mentoring, Bachelor-/Master Theses (see also)
Currently assigned topics
Finished topics
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?
See also: Merkblatt für externe Arbeiten des Prüfungsamtes.
Recommendation Letters/Empfehlungsschreiben
Recommendation letters are a common requirement for applications to top universities, notably in the US. If you consider asking me for such a letter, please make sure that I can offer concrete evidence of your qualifications that goes beyond your course grades. Just taking part in my lecture is not sufficient and the resulting letter would typically be too generic to actually be favorable for your application.
Examples for such evidence could be: you have worked as a Hiwi/Tutor within the SoSy-Lab or you did a thesis/project/seminar with us. Perhaps in some cases very good exercise solutions can count, too.
Research
Relational Proofs
The goal is to infer simulation relations and invariants to prove that two implementations of the same interface exhibit the same external behavior (i.e., Liskov and Wing’s substitution principle).
Notably, we focus on complex data types such as Arrays and Lists in combination where simulation relations often need to be defined by recursion with the help of quantifiers.
Joint work with Grigory Fedyukovich.
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–2022).
Co-supervised with Ben Rubinstein, Toby Murray (University of Melbourne).
Software
- Cuvée: SMT-LIB with programs and weakest preconditions, draft.
- Korn: Horn-clause based verifier for C, draft.
- Legion/SymCC: tight integration of concolic execution and fuzzing.
- SecC: verified information flow for C.
- FalStar: hybrid systems falsification.
- Easyparse: LL parsing for Scala case classes made simple.
Service
Editorial Board:
PC co-chair:
- PhD Symposium @ iFM 2023
- FTfJP 2019 at ECOOP 2019
Organizer/Co-organizer:
- AVM 2022
- Mentoring Workshop @ ETAPS 2022
- ARCH 2019–
- VerifyThis Long Term Challenge Series
- VerifyThis 2018
PC:
- Formalise 2023
- HSCC 2021
- VSTTE 2020
- SAC 2020
- 4PAD 2019
- SAC 2019
- 4PAD 2018
- Artifact Evaluation: HSCC 2020, SAS 2018