Advertisement
Published in:
2009 | OriginalPaper | Chapter
A Formalisation of Smallfoot in HOL
Author : Thomas Tuerk
Published in: Theorem Proving in Higher Order Logics
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In this paper a general framework for separation logic inside the HOL theorem prover is presented. This framework is based on Abstract Separation Logic. It contains a model of an abstract, imperative programming language as well as an abstract specification logic for this language. While the formalisation mainly follows the original definition of Abstract 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.