Data structures are useful is large software systems, because they provide mechanisms for persistence and abstraction. However, these benefits are exactly what make verification difficult. Because data structures provide persistence, one must ensure they are always safe. Because data structures provide abstraction, the safety of the overall system can sometimes rely on these abstractions being maintained.
To verify data structures in the presence of persistence and abstraction, one must find a representation invariant. These representation invariants are predicates over the data structures, and act as fixpoints over data structure operations. Hanoi tackles the problem of generating these representation invariants.
UCLA
Princeton
UT AustinAnders Miltner, Saswat Padhi, Todd Millstein, and David Walker. Data-Driven Inference of Representation Invariants. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '20), June 2020. [ conference version ]
This project is supported in part by NSF grant CCF-1837129 and a PhD fellowship from Microsoft Research. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the NSF or Microsoft Research.
