This paper presents a novel automated procedure for discovering expressive shape specifications for sophisticated functional data structures. Our approach extracts potential shape predicates based on the definition of constructors of arbitrary user-defined inductive data types, and combines these predicates within an expressive first-order specification language using a lightweight data-driven learning procedure. Notably, this technique requires no programmer annotations, and is equipped with a type-based decision procedure to verify the correctness of discovered specifications. Experimental results indicate that our implementation is both efficient and effective, capable of automatically synthesizing sophisticated shape specifications over a range of complex data types, going well beyond the scope of existing solutions.
Thu 16 JunDisplayed time zone: Tijuana, Baja California change
15:30 - 17:00 | |||
15:30 30mTalk | Just-in-Time Static Type Checking for Dynamic Languages Research Papers Brianna M. Ren University of Maryland, College Park, Jeffrey S. Foster University of Maryland, College Park Media Attached | ||
16:00 30mTalk | Types from data: Making structured data first-class citizens in F# Research Papers Tomas Petricek University of Cambridge, UK, Don Syme Microsoft, Gustavo Guerra Microsoft Corporation, London Pre-print Media Attached | ||
16:30 30mTalk | Automatically Learning Shape Specifications Research Papers He Zhu Purdue University, Gustavo Petri LIAFA, Université Paris Diderot, Suresh Jagannathan Purdue University Media Attached |