Paper accepted at CAV: SecCSL: Security Concurrent Separation Logic

Prof. Dr. Gidon Ernst

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
Phone
+49 (89) 2180-9376
E-Mail
firstname.lastname@sosy.ifi.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, Twitter

News

  • CAV paper accepted! Gidon Ernst and Toby Murray: SecCSL: Security Concurrent Separation Logic.
    ( paper draft, supplementary material).
  • SecC: A verifier for C that supports expressive information flow and concurrency.

Research

Publications

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

Service

Teaching