|
A
Separation
Logic
Framework
for
Imperative
HOL
Title: |
A Separation Logic Framework for Imperative HOL |
Author: |
Peter Lammich and Rene Meis (rene /dot/ meis /at/ uni-due /dot/ de) |
Submission date: |
2012-11-14 |
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.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Automatic_Refinement, Collections |
Used by: |
ROBDD, Refine_Imperative_HOL, UpDown_Scheme |
Status: [ok] |
This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|