Project | Informatics


A verifier for programs using stored procedures

Sponsored by Project From Reasoning Principles for Function Pointers To Logics for Self-Configuring Programs" (EP/G003173/1)
The University of Sussex
EPSRC Research Funding
[ Crowfoot Team ]
Billiejoe Charlton
Benjamin Horsfall
Bernhard Reus (PI)
[ Crowfoot tool ]
Crowfoot is a semi-automated verification tool we have developed for reasoning about programs which store procedures/code on the heap. Crowfoot uses symbolic execution based on separation logic (a technique introudced in Smallfoot) to reason about programs, proving that procedures meet their specifications, which the user provides in the form of pre- and post-conditions. Crucially, the assertion language of Crowfoot includes the nested triples developed by Schwinghammer, Birkedal, Reus and Yang. This is what allows us to reason in a modular way about the behaviour of code stored on the heap.
[ Crowfoot Description ]
A short description here.
The VMCAI 2012 paper.
[ Using Crowfoot ]
You can try Crowfoot here using the web-based version, where it is possible to verify a series of examples and examine the graphical output.

[ Crowfoot Example: Webserver Details ]
For help understanding the graphs that Crowfoot produces, see this explanation of the updatable webserver example that can also be run on the web-based version (see item above).

Page maintained by Crowfoot Team
Logo by Simon Fleming