Email Gateway (Aug 19 2022 at 09:21): Email Gateway (Aug 19 2022 at 09:21):From: Tobias Nipkow <nipkow@in.tum.de>
Peter Lammich and Rene Meis
http://afp.sourceforge.net/entries/Separation_Logic_Imperative_HOL.shtml
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.
Enjoy!
Last updated: Nov 21 2024 at 12:39 UTC