Discovering relational specifications
Discovering relational specifications
复制标题
DOI：
10.1145/3106237.3106279
复制
发表时间：
2017-08
期刊：
影响因子：
--
通讯作者：
Calvin Smith;G. Ferns;Aws Albarghouthi
中科院分区：
文献类型：
--
作者：
Calvin Smith;G. Ferns;Aws Albarghouthi
图书馆功能的形式规格在许多程序分析和开发任务中起着至关重要的作用。我们提出了Bach，这是一种从描述包含库或程序的一组功能的输入输出行为的数据中发现可能的关系规格的技术。关系规格将不同函数的不同执行相关联；例如，交通量，传递性，两个函数的等效性等等。我们将BACH应用于为许多标准库生成的数据学习规格。我们的实验评估表明，巴赫在少量时间内学习有用和深度规格的能力。
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.