Verification and Synthesis for Data Structures - Anders Miltner
Workshop on Dependable and Secure Software Systems 2021
Data structures provide safe mechanisms to maintain and organize data. But it does so at a cost: to obtain this safety, data structures necessitate representation invariants, predicates over the underlying data stores. To verify that a data structure is correct one must first identify a representation invariant. Furthermore, if one is to synthesize new functions for that data structure, one must ensure that the generated code does not break its invariants. In this talk, I will present two tools: Hanoi and Burst. Hanoi automatically generates representation invariants for a data structure, given a set of theorems about how that data structure should behave. Burst takes a logical specification as input and outputs a function satisfying that specification. This enables generating functions that are guaranteed to respect data structure invariants. Lastly, I will present some general approaches on how to use these tools for full data-structure inference.