Beta 1


Title Specification and validation of data structures using separation logic
Author Braband Jensen, Jonas
Supervisor Probst, Christian W. (Language-Based Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2010
Abstract This report presents the results of a case study in formal specification and verification using separation logic of the linked list with views data structure as found in the C5 library of collections for .NET. A view can be thought of as a generalisation of an iterator. This data structure is interesting for verification purposes because it makes extensive use of pointers and shared data on the heap. The public methods of lists and views are given formal specifications by relating their behaviour to manipulations of a mathematical object. These specifications lead to a deeper understanding of linked lists with views and reveal several peculiar corner cases. Parts of a reimplementation of the method bodies are then proved to satisfy their specifications. To support this reasoning formally, a separation logic dialect is developed whose most prominent feature is an encoding of fractional permissions that is more general in some respects than what is found elsewhere in the literature. All of this leads to discussions on the benefits and drawbacks of separation logic and its various extensions in the situations encountered. Many ideas for future work are suggested, both for the separation logic framework and for the data structure.
Imprint Technical University of Denmark (DTU) : Kgs. Lyngby, Denmark
Series IMM-M.Sc.-2010-07
Fulltext
Original PDF ep10_07.pdf (1.24 MB)
Admin Creation date: 2010-03-08    Update date: 2010-10-28    Source: dtu    ID: 258989    Original MXD