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. |
BibTeX: |
@article{Separation_Logic_Imperative_HOL-AFP,
author = {Peter Lammich and Rene Meis},
title = {A Separation Logic Framework for Imperative HOL},
journal = {Archive of Formal Proofs},
month = nov,
year = 2012,
note = {\url{http://isa-afp.org/entries/Separation_Logic_Imperative_HOL.html},
Formal proof development},
ISSN = {2150-914x},
}
|