Please use this identifier to cite or link to this item:
|Title:||That’s correct: Using the Verified Software Toolchain to verify C maps|
|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.|
|Type of Material:||Princeton University Senior Theses|
|Appears in Collections:||Computer Science, 1988-2016|
Files in This Item:
|PUTheses2015-Yucht_Miles.pdf||623.11 kB||Adobe PDF||Request a copy|
Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.