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 Jun Times are displayed in 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. RenUniversity of Maryland, College Park, Jeffrey S. FosterUniversity of Maryland, College Park Media Attached | ||
16:00 30mTalk | Types from data: Making structured data first-class citizens in F# Research Papers Tomas PetricekUniversity of Cambridge, UK, Don SymeMicrosoft, Gustavo GuerraMicrosoft Corporation, London Pre-print Media Attached | ||
16:30 30mTalk | Automatically Learning Shape Specifications Research Papers He ZhuPurdue University, Gustavo PetriLIAFA, Université Paris Diderot, Suresh JagannathanPurdue University Media Attached |