Crowfoot: a verifier for higher-order store programs

Charlton, Nathaniel, Horsfall, Ben and Reus, Bernhard (2012) Crowfoot: a verifier for higher-order store programs. In: Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, 7148 . Springer, pp. 136-151. ISBN 978-3-642-27940-9

[img] PDF
Restricted to SRO admin only

Download (438kB)

Abstract

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.

Item Type: Book Section
Additional Information: 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Bernhard Reus
Date Deposited: 14 May 2013 15:29
Last Modified: 14 Nov 2013 10:46
URI: http://sro.sussex.ac.uk/id/eprint/31151

View download statistics for this item

📧 Request an update