Crowfoot: A verifier for higher-order store programs. We present Crowfoot, an automatic verification tool for imperative programs that manipulate procedures dynamically at runtime; these programs use a heap that can store not only data but also code (commands or procedures). Such heaps are often called higher-order store, and allow for instance the creation of new recursions on the fly. One can use higher-order store to model phenomena such as runtime loading and unloading of code, runtime update of code and runtime code generation. Crowfoot’s assertion language, based on separation logic, features nested Hoare triples which describe the behaviour of procedures stored on the heap. The tool addresses complex issues like deep frame rules and recursion through the store, and is the first verification tool based on recent developments in the mathematical foundations of Hoare logics with nested triples.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben: Symbolic execution proofs for higher order store programs (2015)
- Charlton, Nathaniel; Reus, Bernhard: Specification patterns for reasoning about recursion through the store (2013)
- Charlton, Nathaniel; Horsfall, Ben; Reus, Bernhard: Crowfoot: a verifier for higher-order store programs (2012)
- Charlton, Nathaniel; Reus, Bernhard: Specification patterns and proofs for recursion through the store (2011)
- Schwinghammer, Jan; Birkedal, Lars; Reus, Bernhard; Yang, Hongseok: Nested Hoare triples and frame rules for higher-order store (2011)