A Formalisation of Smallfoot in HOL

In this paper a general framework for separation logic inside the HOL theorem prover is presented. This framework is based on Abeparation Logic. It contains a model of an abstract, imperative ing language as well as an abstract specification logic for this language. While the formalisation mainly follows the original definition act Separation Logic, it contains some additional features. Most noticeably is added support for procedures. As a case study, the framework is instantiated to build a tool that is able to parse Smallfoot specifications and verify most of them completely automatically. In contrast to Smallfoot this instantiation can handle the content of data-structures as well as their shape. This enables it to verify fully functional specifications. Some noteworthy examples that have been verified are parallel mergesort and an interactive filter-function for single linked lists. 1 Motivation Separation logic is an extension of Hoare logic that allows local reasoning [7, 9...

• Type: Conference
• Year: 2009
• Where: TPHOL
• Authors: Thomas Tuerk
• Keywords: Act Separation Logic, Artificial Intelligence, Hoare Logic, Separation Logics, TPHOL 2009