A Separation Logic Framework for Imperative HOL. 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.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Charguéraud, Arthur; Pottier, François: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (2019)
- Lammich, Peter: Refinement to imperative HOL (2019)
- Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
- Zhan, Bohua: Efficient verification of imperative programs using auto2 (2018)
- Zhan, Bohua; Haslbeck, Maximilian P. L.: Verifying asymptotic time complexity of imperative programs in Isabelle (2018)
- Lammich, Peter; Sefidgar, S. Reza: Formalizing the Edmonds-Karp algorithm (2016)
- Lammich, Peter: Refinement to Imperative/HOL (2015)