Dr. Gidon Ernst

Gidon Ernst





  • 1986: born in Freiburg im Breisgau
  • 2004: Abitur, Marie-Curie-Gymnasium, Kirchzarten
  • 2008: Bachelor of Science in Informatics, University of Freiburg: Introducing Threads into the TakaTuka Java Virtual Machine
  • 2010: Master of Science in Software Engineering (Elite Graduate Program), University of Augsburg: Shape Analysis of Regular Pointer Structures
  • Since 2010: Researcher at the Institute for Software and Systems Engineering, University of Augsburg, Group of Prof. Dr. Reif


My research focuses on the application of formal methods to the construction of verififed software, including the topics
  • Formal methods, refinement, correctness by construction
  • Modular verification technology for complex properties such as power-cut safety
  • Techniques for linked structures, e.g., separation logic/shape analysis
  • Interactive & automated theorem proving, tool support and applications (see the KIV System and try it out)

I am involved in the Flashix-Project that develops a fully verified file system for Flash memory. See the technical description and the github repository for further details.

Our group has successfully participated in several verification competitions, see VerifyThis@ETAPS'15 (best student team with Jörg Pfähler), vscomp'14, VerifyThis@FM'12 (best student team with Jörg Pfähler), vscomp'12, Cost Competition@FoVeOOS'11, and our solutions.


  • Formale Methoden im Software Engineering, Lab (since 2011)
  • Seminars: Systemmodellierung und Verifikation (Master), Moderne Entwurfsmethoden für Innovative Softwaresysteme (Bachelor), Software & Systems Engineering (Bachelor)
  • Supervision of Bachelor/Master theses