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.