Princeton University Library Catalog

That’s correct: Using the Verified Software Toolchain to verify C maps

Author/​Artist:
Yucht, Miles [Browse]
Format:
Senior thesis
Language:
English
Advisor(s):
Appel, Andrew [Browse]
Department:
Princeton University. Department of Computer Science [Browse]
Class year:
2015
Description:
53 pages
Summary note:
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.