A Separation Logic Framework for Imperative HOL

Peter Lammich 🌐 and Rene Meis 📧 with contributions from Valentin Springsklee 📧

November 14, 2012

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We provide a framework for separation-logic based correctness proofs of Imperative HOL programs. Our framework comes with a set of proof methods to automate canonical tasks such as verification condition generation and frame inference. Moreover, we provide a set of examples that show the applicability of our framework. The examples include algorithms on lists, hash-tables, and union-find trees. We also provide abstract interfaces for lists, maps, and sets, that allow to develop generic imperative algorithms and use data-refinement techniques.
As we target Imperative HOL, our programs can be translated to efficiently executable code in various target languages, including ML, OCaml, Haskell, and Scala.

License

BSD License

Topics

Session Separation_Logic_Imperative_HOL