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

Projects

current

older

Events

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).

  • 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
    (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)