Gidon is a postdoc researcher at the Mathematical and Metamathematical Modeling group lead by Prof. Dr. Ichiro Hasuo at the National Institute of Informatics, Tokyo.

**Email**: gidonernst (*) gmail.com

- ERATO Metamathematics for Systems Design (PI: Prof. Dr. Ichiro Hasuo). In this project, mathematical techniques for the design and analysis of hybrid systems are researched. The focus lies on the automotive domain, which is under increasing pressure to achieve highly reliability despite the growing complexity. In addition to traditional correctness concerns from software engineering, additional aspects such as timing or stochastic guarantees are considered. The unique strategy of the project is based on meta-mathematical transfer: fundamental principles behind the extension of and combination with existing formal methods techniques by these new concerns are researched.

Flashix (project, github, PI: Prof. Dr. Wolfgang Reif) is the first fully verified POSIX-Complicant file system for flash memory. It has a complete but abstract functional specification, that is broken down to an efficient implementation by incremental refinement and a formal proof done. Development was done in the KIV system and proven functionally correct and power cut safe.

KIV is a tool for formal systems development and interactive verification. It can be employed, e.g., for the development of safety critical systems from formal requirements specifications down to executable code. KIV can handle large scale formal models by efficient proof techniques, multi-user support, and an ergonomical user interface, and an integration into the Eclipse software platform. It has been used in a number of industrial pilot applications, in international verification competitions, and in teaching.

Combination of shape analysis and theorem proving (project, github). Goal of this research was to integrate automated shape analysis tools into the interactive software verification workflow to increase automation. As a case study, an implementation of B+ trees was verified. Using an integration of the tools TVLA and KIV, it was proven that insertion and deletion preserve all of the B+ tree invariants (tree structure, height-balance, sortedness) and that the operations correspond to counterparts on a set-based abstraction. Soundness of the integration was proved on a semantic meta-level.

- Artifact evaluation: SAS 2018
- Co-organizer: VerifyThis 2018
- PC: 4PAD 2018,

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

*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 (accepted, 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.

*Modular verification of order-preserving writeback caches*

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

In Proc. of 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.