# 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. They have open positions, consider applying!

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

- Formal Techniques for Java-like Programs (FTfJP) at ECOOP 2019

- Formal Approaches to Parallel and Distributed Systems (4PAD) at HPCS 2019

**submission deadline: March 1, 2019** - VerifyThis 2018 program verification competition report
- FalStar: fast falsification for hybrid systems (on arXiv), see also ARCH friendly competition

## Projects

### current

- COVERN: compositional verification and refinement of noninterference

(with Toby Murray) - FalStar: falsification of temporal logic requirements for 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

- FTfJP 2019 2019 (program co-chair)
- 4PAD 2019 at HPCS 2019 (program commitee)
- ARCH 2019 falsification category (co-organizer, competition participant)
- TOOLympics 2019 at TACAS 2019
- SAC 2019 (program commitee)
- SAS 2018 (artifact evaluation)
- ARCH 2018 (competition participant)
- VerifyThis 2018 (co-organizer)

## Publications

### articles

*Two-Layered Falsification of Hybrid Systems guided by Monte Carlo Tree Search*

Z. Zhang, G. Ernst, S. Sedwards, P. Arcaini, I. Hasuo.

Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD),

Special issue for the International Conference on Embedded Software (EMSOFT), 2018 (doi, arXiv).

**nominated for best paper***Unifying separation logic and region logic to allow interoperability*

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

Formal Aspects of Computing (FAC) 2018 (doi).*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

*ARCH-COMP18 Category Report: Results on the Falsification Benchmarks*

A. Dokhanchi, S. Yaghoubi, B. Hoxha, G. Fainekos, G. Ernst, Z. Zhang, P. Arcaini, I. Hasuo and S. Sedwards.

Applied Verification of Continuous and Hybrid Systems (ARCH), 2018 (doi).*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 (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.

**best paper***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)