Charge! A framework for higher-order separation logic in Coq. We present a comprehensive set of tactics for working with a shallow embedding of a higher-order separation logic for a subset of Java in Coq. The tactics make it possible to reason at a level of abstraction similar to pen-and-paper separation-logic proof outlines. In particular, the tactics allow the user to reason in the embedded logic rather than in the concrete model, where the stacks and heaps are exposed. The development is generic in the choice of heap model, and most of the development is also independent of the choice of programming language.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Bannister, Callum; Höfner, Peter; Klein, Gerwin: Backwards and forwards with separation logic (2018)
- Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W.: VST-Floyd: a separation logic tool to verify correctness of C programs (2018)
- Paviotti, Marco; Bengtson, Jesper: Formally verifying exceptions for low-level code with separation logic (2018)
- Charguéraud, Arthur; Pottier, François: Temporary Read-only permissions for separation logic (2017)
- Georges, Aina Linn; Murawska, Agata; Otis, Shawn; Pientka, Brigitte: \textscLincx: a linear logical framework with first-class contexts (2017)
- Malecha, Gregory; Bengtson, Jesper: Extensible and efficient automation through reflective tactics (2016)
- Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
- Dodds, Josiah; Appel, Andrew W.: Mostly sound type system improves a foundational program verifier (2013)
- Bengtson, Jesper; Jensen, Jonas Braband; Birkedal, Lars: Charge! A framework for higher-order separation logic in Coq (2012)