Automatically learning shape specifications

He Zhu, Gustavo Petri, Suresh Jagannathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationPLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsChandra Krintz, Emery Berger
PublisherAssociation for Computing Machinery
Pages491-507
Number of pages17
ISBN (Electronic)9781450342612
DOIs
StatePublished - Jun 2 2016
Externally publishedYes
Event37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016 - Santa Barbara, United States
Duration: Jun 13 2016Jun 17 2016

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Volume13-17-June-2016

Conference

Conference37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016
Country/TerritoryUnited States
CitySanta Barbara
Period6/13/166/17/16

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Data structure verification
  • Learning
  • Refinement types
  • Shape analysis
  • Testing

Fingerprint

Dive into the research topics of 'Automatically learning shape specifications'. Together they form a unique fingerprint.

Cite this