Skip navigation
Please use this identifier to cite or link to this item:
Title: That’s correct: Using the Verified Software Toolchain to verify C maps
Authors: Yucht, Miles
Advisors: Appel, Andrew
Department: Computer Science
Class Year: 2015
Abstract: Here, I present the formal verifications of two implementations of the map abstract data type between integer values, one as a linked list and one as a hashtable whose buckets are linked lists. The linked list and hashtable programs are written in Verifiable C. To verify these programs, I develop a formalization for the finite map data structure based on functions with domain A and range option B, where A, B are types. Then, I prove several lemmas which relate abstract finite maps to Coq data structures; this so-called representation relation of the abstract map is used to link finite maps to separation logic predicates, which allow one to formally make an assertion such as "there exists a map m at memory location l." Using these predicates, I create a set of formal specifications for the linked-list program, and then I prove that the linked-list program obeys these specifications. Then, I generalize the linked-list specification so that it can be used to describe the hashtable implementation as well, and using this generalized specification, I prove the correctness of the hashtable implementation. Finally, I present a brief usability review of the VST, highlighting the success and failures in my experience using the VST.
Extent: 53 pages
Type of Material: Princeton University Senior Theses
Language: en_US
Appears in Collections:Computer Science, 1988-2020

Files in This Item:
File SizeFormat 
PUTheses2015-Yucht_Miles.pdf623.11 kBAdobe PDF    Request a copy

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.