In this paper we present a stepwise refinement based top-down approach to verified imperative data structures. Our approach is modular in the sense that already verified data structures can be used for construction of more complex data structures. Moreover, our data structures can be used to verify real algorithms. Our tool chain supports refinement down to executable code in various programming languages, and is fully implemented in Isabelle/HOL, such that its trusted code base is only the inference kernel and code generator of Isabelle/HOL.

As a case study, we verify an indexed heap data structure, and use it to generate an efficient verified implementation of Dijkstra’s algorithm.

I am a researcher (post-doc) at the chair for logic and verification of Prof. Tobias Nipkow. My main research interest is the production of verified software by a top-down refinement process. For this, I’m using the theorem prover Isabelle/HOL, for which I have developed the Isabelle Refinement Framework and the Isabelle Collection Framework. Other research interests include the automatic analysis of models for concurrent programs, and the mechanical verification of the analysis algorithms. To this end, I have explored dynamic pushdown networks, a model for concurrent programs with thread creation and locks as synchronization primitive. Moreover, we have developed the fully verified CAVA LTL model checker. Recently, I have also worked on modeling web-services in Isabelle/HOL, and formally verifying their information flow security properties. As a demonstrator, we have developed the conference management system CoCon, that has formally verified information flow properties