June 10, 2020
Congratulations to PhD student Anders Miltner, and coauthors Saswat Padhi (UCLA), Professor Todd Millstein (UCLA), and Professor David Walker for their paper entitled "Data-driven inference of representation invariants," which won a PLDI 2020 distinguished paper award.
Given a specification for a module, Anders develops a new algorithm for inferring representation invariants for that module, ie, constraints defining the data structures the module generates. Such representation invariants are usually a key component of a module's proof of correctness. The key novelty of the work is a type-directed notion of "visible inductiveness," which ensures that the algorithm makes consistent progress towards its goal as it alternates between weakening and strengthening candidate invariants.
The 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020) is set to take place virtually for the first time. Anders will present his research in a talk at 8:00am Pacific time on Wednesday, June 17th.