# Gidon Ernst

Postdoc Fellow

Computing and Information Systems

University of Melbourne

Office 8.14, Doug McDonell Building

Email: gidon.ernst (*) unimelb.edu.au

I am a postdoc fellow with Toby Murray at the University of Melbourne. I completed my doctorate in 2016 at the University of Augsburg under the supervision of Wolfgang Reif. I spent about a year as a postdoc in the ERATO Metamathematics for Systems Design lead by Ichiro Hasuo at NII, Tokyo.

My research focuses in scalable methods for software specification, testing, and verification. I am specifically intested 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.

## News

- May 2018: Falsification tool for hybrid systems available (beta)
- April 2018: VerifyThis 2018 program verification competition at ETAPS

## Projects

### current

- COVERN: compositional verification and refinement of noninterference

(with Toby Murray) - Falsification of hybrid systems

(with Ichiro Hasuo, Sean Sedwards, Zhenya Zhang)

### older

- 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

## Events

- SAS 2018 (artifact evaluation)
- ARCH 2018 (competition participant)
- SNR 2018
- VerifyThis 2018 (co-organizer)
- 4PAD 2018 (program commitee)

## Publications

### articles

*Symbolic Execution for a Clash-Free Subset of ASMs*

G. Schellhorn, G. Ernst, J. Pfähler, Stefan Bodenmüller, and W. Reif.

Science of Computer Programming (SCP), 2017 (doi, pdf).*Modular, crash-safe refinement for ASMs with submachines*

G. Ernst, J. Pfähler, G. Schellhorn, and W. Reif.

Science of Computer Programming (SCP), 2016 (pdf).*KIV—Overview and VerifyThis competition*

G. Ernst, J. Pfähler, G. Schellhorn, D. Haneberg, and W. Reif.

Software Tools for Technology Transfer (STTT), 2015.*RGITL: A temporal logic framework for compositional reasoning about interleaved programs*

G. Schellhorn, B. Tofan, G. Ernst, J. Pfähler, and W. Reif.

Annals of Mathematics and Artificial Intelligence (AMAI), 2014.*Verification of B+ trees by integration of shape analysis and interactive theorem proving*

G. Ernst, G. Schellhorn, and W. Reif.

Software & Systems Modeling (SOSYM), 2015.

### in proceedings

*Time-staging Enhancement of Hybrid System Falsification.*

G. Ernst, I. Hasuo, Z. Zhang, and S. Sedwards.

In Proc. of Symbolic and Numerical Methods for Reachability Analysis (SNR), 2018

(to appear, preprint, arXiv).*Modular verification of order-preserving writeback caches*

J. Pfähler, G. Ernst, S. Bodenmüller, G. Schellhorn, and W. Reif.

Integrated Formal Methods (iFM), 2017 (pdf).*A relational encoding for a clash-free subset of ASMs*

G. Schellhorn, G. Ernst, J. Pfähler, and W. Reif.

Alloy, ASM, B, TLA, VDM, and Z (ABZ), 2016 (pdf).*Inside a verified Flash file system: transactions & garbage collection*

G. Ernst, J. Pfähler, G. Schellhorn, and W. Reif.

Verified Software: Theories, Tools, Experiments (VSTTE), 2015 (pdf).*Conditional effects in fine-grained region logic*

Y. Bao, G. T. Leavens, and G. Ernst.

Formal Techniques for Java-like Programs (FTfJP), 2015.*Modular refinement for submachines of ASMs*

G. Ernst, J. Pfähler, G. Schellhorn, and W. Reif.

Alloy, ASM, B, TLA, VDM, and Z (ABZ), 2014 (pdf).*Development of a verified Flash file system*

G. Schellhorn, G. Ernst, J. Pfähler, D. Haneberg, and W. Reif.

Alloy, ASM, B, TLA, VDM, and Z (ABZ), 2014 (invited paper, pdf).*Verification of a Virtual Filesystem Switch*

G. Ernst, G. Schellhorn, D. Haneberg, J. Pfähler, and W. Reif.

Verified Software: Theories, Tools, Experiments (VSTTE), 2013 (pdf).*Compositional verification of a lock-free stack with RGITL*

Tofan B, G. Schellhorn, Gidon G. Ernst, J. Pfähler, and W. Reif.

Electronic Communications of the Automated Verification of Critical Systems (EASST), 2014.*Formal specification of an erase block management layer for Flash memory*

J. Pfähler, G. Ernst, G. Schellhorn, D. Haneberg, and W. Reif.

In Haifa Verification Conference (HVC), 2013 (pdf).*A formal model of a Virtual Filesystem Switch*

G. Ernst, G. Schellhorn, D. Haneberg, J. Pfähler, and W. Reif.

Software and Systems Modeling (SSV), 2012 (pdf).*Verification of B+ trees: an experiment combining shape analysis and interactive theorem proving*

G. Ernst, G. Schellhorn, and W. Reif.

Software Engineering and Formal Methods (SEFM), 2011 (pdf).*Interleaved programs and rely-guarantee reasoning with ITL*

G. Schellhorn, B. Tofan, G. Ernst, and W. Reif.

Temporal Representation and Reasoning (TIME), 2011.*Simulating a Flash File System with CoreASM and Eclipse*

M. Junker, D. Haneberg, G. Schellhorn, W. Reif, and G. Ernst.

Dependable Software for Critical Infrastructures (DSCI), 2011.*The COST IC0701 verification competition 2011*

T. Bormer, M. Brockschmidt, D. Distefano, G. Ernst, J.-C. Filliâtre, R. Grigore, M. Huisman, V. Klebanov, C. Marché, R. Monahan, W. Mostowski, N. Polikarpova, C. Scheben, G. Schellhorn, B. Tofan, J. Tschannen, and M. Ulbrich.

Formal Verification of Object-Oriented Software (FoVeOOS), 2011.*Optimized java binary and virtual machine for tiny motes*

F. Aslam, L. Fennell, C. Schindelhauer, P. Thiemann, G. Ernst, E. Haussmann, S. Rührup, and Z. A. Uzmi.

Distributed Computing in Sensor Systems (DCOSS), 2010.

### thesis

*A Verified POSIX-Compliant Flash File System - Modular Verification Technology & Crash Tolerance*

G. Ernst, PhD thesis, reviewers: W. Reif, A. Knapp, J. Derrick, Augsburg University, 2016. (pdf)