Discovering relational specifications

Calvin Smith, Gabriel Ferns, Aws Albarghouthi

Abstract

Formal specifications of library functions play a critical role in a number of program analysis and development tasks. We present Bach, a technique for discovering likely relational specifications from data describing input-output behavior of a set of functions comprising a library or a program. Relational specifications correlate different executions of different functions; for instance, commutativity, transitivity, equivalence of two functions, etc. Bach combines novel insights from program synthesis and databases to discover a rich array of specifications. We apply Bach to learn specifications from data generated for a number of standard libraries. Our experimental evaluation demonstrates Bach's ability to learn useful and deep specifications in a small amount of time.

BibTeX

@inproceedings{Smith-al:FSE17,
  author    = {Calvin Smith and
               Gabriel Ferns and
               Aws Albarghouthi},
  title     = {Discovering relational specifications},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {616--626},
  publisher = {{ACM}},
  year      = {2017},
}

Discovering relational specifications

Abstract

Related papers