M.Sc. Gidon Ernst
Research & Activities
My research focuses on the application of formal methods to the construction of verififed software, including the topics
- Refinement, correctness by construction
- Techniques for linked structures, e.g., separation logic/shape analysis
I am involved in the Flashix
-Project that develops a fully verified file system for Flash memory.
Our group has participated in several verification competitions, see