A Heap of Problems
From A Heap of Problems
Separation logic and shape analysis are powerful tools for verifying specifications of programs which manipulate dynamically-allocated data structures. There are good tools available that are able to verify interesting specifications even automatically. To mention just a few, there are:
However, these tools usually consider just the shape of data structures while neglecting their content. Full functional verification remains a challenge.
This site tries to help answering this challenge by collecting benchmark examples. This is done in the hope that this set of examples will simplify communication between different developers and enable them to compare their tools and approaches more easily.
Currently, most of the examples are extended and slightly modified Smallfoot examples. They are used here by courtesy of Hongseok Yang, Peter O'Hearn, Christiano Calcagno and Josh Berdine. That's why most examples come with a pseudo-code description similar to the one use by Smallfoot. However, there is a C-code and a natural language description as well.
Besides the problems the proofs done using different tools are published here as well.
This example collection is implemented as a Wiki. Please add comments on examples, your own examples, tool descriptions,
proofs and proof sketches and whatevery you think might be interesting for this Wiki. Unluckily the access had to the Wiki had to be restricted
due to spam. Please contact Thomas Tuerk to get an account.
For questions on how to use the Wiki, you can refer to MediaWiki User's Guide.
For all other questions please contact Thomas. He is also willing to add some content for you, if you prefer not
to have an own account and use the Wiki.
Example Structure
All examples consist of
- a high-level, natural language description of the algorithm and its specification,
- a C-implementation and
- a pseudo-code implementation with specification,
- possibly some proofs or discussions.
The pseudo-code implementation is written in the language used by Smallfoot. It contains specifications and loop-invariants in Smallfoot's specification language. These specifications do not mention data. This allows Smallfoot to automatically verify them. However, specifications and loop-invariants that do mention data are added as comments. An explanation of Smallfoot's syntax can be found here.
In contrast to the pseudo-code implementations, the C-implementations do not contain specifications. Instead, they come with some testing code. The implementations of the examples share some code, e.g. the definition of a data-structure for single-linked-lists. An explanation of this infrastructure can be found here.