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
- Mi-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
Curriculum vitae, Google Scholar, DBLP, ORCID, Github, TwitterPublications
News
-
New Publication:
Gidon Ernst and Toby Murray: SecCSL: Security Concurrent Separation Logic.
CAV 2019.
Draft,
Slides.
- 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).
-
Paper accepted:
Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo:
Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input.
To appear at QEST 2019.
Draft.
- 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.
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.
SecCSL
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.
Joint work with Toby Murray
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.
Previous Projects
- Flashix: verified file system for flash memory
(github, with Wolfgang Reif, Gerhard Schellhorn, Jörg Pfähler, Stefan Bodenmüller) - KIV: interactive theorem prover and software verification platform (see also VerifyThis)
- IMP3: integration of shape analysis and theorem proving
- Takatuka: Java Virtual Machine for sensor networks
Service
- PC co-chair: FTfJP 2019 at ECOOP 2019
- Co-organizer: ARCH 2019, VerifyThis 2018
- PC: SAC 2020, 4PAD 2019, SAC 2019, SAS 2018 (artifact evaluation), 4PAD 2018