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
- Do/Fr, by appointment
- Phone
- +49 (89) 2180-9376
- 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
Personal
CV, Publications, Google Scholar, DBLP, ORCID, Github, Twitter
News
- Talk at the CPAchecker workshop 2019 on VerifyThis challenges in sv-benchmarks. Slides, SV-COMP 2020.
- Call for Papers: SAC 2020 - Software Verification and Testing Track. Extended deadline: September 29!
- 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)
- Softwaretechnik (3+2)
- Einführung in die Informatik: Programmierung und Softwareentwicklung für Nebenfach (3+1+2)
- Masterseminar "Fuzz Testing" (2)
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.
Joint 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
- 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, ARCH 2019, VerifyThis 2018
- PC: SAC 2020, 4PAD 2019, SAC 2019, SAS 2018 (artifact evaluation), 4PAD 2018