Starfoot: Smallfoot in jStar

Separation logic is a logic for reasoning about data-structures such as linked lists. It permits local reasoning, meaning that properties of programs can be proved by only looking at the parts of memory that they manipulate, and ignoring parts they don't access. Smallfoot is an automatic tool that checks separation logic specifications. Smallfoot focusses exclusively on programs that manipulate linked lists.

jStar is a new tool developed in Cambridge intended to generalise many of the techniques used in Smallfoot. jStar provides a back-end for checking specifications for any kind of data-structure, and a core language into which any language can be translated. jStar was developed to verify Java, but it is currently being extended to verify programs in a variety of languages and domains.

In this project, I propose that you develop a Smallfoot front-end for jStar. The aim of this project will be to create a usable tool for verifying linked-list programs. jStar is currently under very active development, and this project will involve working alongside the developers of the tool.This project would be an ideal springboard for students interested in pursuing a PhD in the area of program verification.

Please get in contact if you are interested in this project. My address is on the main page.

References:

• The Smallfoot homepage.
• The jStar homepage.
• Separation Logic: A Logic for Shared Mutable Data Structures, John Reynolds. Proceedings of LICS 2002. pp55-74. This paper is a good introduction to separation logic.
• Local Reasoning and Separation Logic. Peter O'Hearn's page links to almost every separation logic paper.