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
|15:30 - 16:00|
Brianna M. RenUniversity of Maryland, College Park, Jeffrey S. FosterUniversity of Maryland, College ParkMedia Attached
|16:00 - 16:30|
Tomas PetricekUniversity of Cambridge, UK, Don SymeMicrosoft, Gustavo GuerraMicrosoft Corporation, LondonPre-print Media Attached
|16:30 - 17:00|
He ZhuPurdue University, Gustavo PetriLIAFA, Université Paris Diderot, Suresh JagannathanPurdue UniversityMedia Attached