We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
Btor2-Select accepted at CAV 2025

Prof. Dr. Gidon Ernst

Junior Professor, Software Verification

Picture of Prof. Dr. Gidon Ernst

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
E-Mail
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

Consider using the keyserver at https://keys.openpgp.org/.

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

  • [11/2024] Presentation: Gidon Ernst: Deductive Verification of Information Flow in Security Concurrent Separation Logic, CS Seminar, University of Konstanz, Slides
  • [10/2024] PC Chair: I am co-chairing SPIN 2025 together with Kristin Yvonne Rozier. Submission dealine: February 13, 2025 via EasyChair
  • [10/2024] Publication: Gidon Ernst, Wolfram Pfeifer, Mattias Ulbrich: Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification, Slides, Draft, DOI, Code, SpecifyThis @ ISoLA 2024
  • [10/2024] Publications in the TOOLympics 2023 series:
    • Ahrendt, Ernst, Herber, Huisman, Monti, Ulbrich, Weigl: The VerifyThis Collaborative Long-Term Challenge Series, DOI
    • Abate, Althoff, Bu, Ernst, Frehse, Geretti, Johnson, Menghi, Mitsch, Schupp, Soudjani: The ARCH-COMP Friendly Verification Competition for Continuous and Hybrid Systems, DOI
  • [09/2024] Presentation: Gidon Ernst, Wolfram Pfeifer, Mattias Ulbrich: Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification, Slides, Alpine Verification Meeting 2024
  • [05/2024] Presentation in the ConVeY Seminar: Deductive Verification & Reasoning Across Abstraction Boundaries, Slides, Dafny examples
  • [04/2024] Results of CHC-COMP 2024 are available, Slides
  • [12/2023] LemmaCalc: Draft, Artifact
  • [11/2023] Publication: Toby Murray, Mukesh Tiwari, Gidon Ernst, David Naumann: Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications, CCS 2023, DOI, Extended Version, Slides, Website, Artifact.
  • [11/2023] Publication: Toby Murray, Pengbo Yan, Gidon Ernst: Compositional Vulnerability Detection with Insecurity Separation Logic, ICFEM 2023, DOI, Extended Version, Artifacts
  • [04/2023] Challenge: Join the VerifyThis long-term collaborative challenge in software specification and verification: https://verifythis.github.io/
  • [04/2023] Publication: Korn—Software Verification with Horn Clauses (Competition Contribution), Paper, GitHub
  • [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.

Lehrveranstaltungen (siehe auch)

Wintersemester 2023/24

Sommersemester 2024

Mentoring, Bachelor-/Master Theses (see also)

Finished topics
Specifying Loops with Contracts. [1]
Information flow testing for PGP keyservers [1]
Implement Fuzzing in CPAchecker
SMT-based checking and synthesis of formal refinements
Rely/Guarantee Reasoning for Separation Logic in SecC
Loop Contracts for Boogie and Dafny
Frontends for a deductive verifier (Python)
Frontends for a deductive verifier (Boogie)
Guided fuzz testing with stochastic optimization
Interactive verification debugging [1]
Simplification and solving strategies for SMT
Development of an interactive theorem prover for untyped logic
User-friendly tactics for interactive proofs
Inference of Invariants over Algebraic Data Types
Test-case generation for protocol implementations via fuzzing
Concolic Testing for Liskov's substitution principle
Studie: PBT Driven Design am Beispiel eines Embedded Software Projekts
Fuzzing Strategies in Legion/SymCC
Symbolic Automata Learning for Unbounded Systems
Case-studies in verifying Python programs
Loop summarization for array programs
Formal Verification of Interactive Visual Novels
Security Specifications for Dafny
Penetration Testing of Web-Applications
Experiments with Inference of Loop Contracts in Dafny

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

PhD Students

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:

Organizer/Co-organizer:

PC: