|
[ 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.
GOTO THE TOOL
|
| |
|
[ 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).
|
