Data-driven inference of representation invariants
Data-driven inference of representation invariants
复制标题
表示不变量的数据驱动推理
DOI：
10.1145/3385412.3385967
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Walker, David
中科院分区：
文献类型：
--
作者：
Miltner, Anders;Padhi, Saswat;Millstein, Todd;Walker, David
表示不变式是一个属性，它保存了由模块产生的所有抽象类型的值。表示不变量在软件工程和程序验证中起着重要的作用。在本文中，我们开发了一个反例驱动的算法，用于推断一个表示不变，这是足以暗示一个模块所需的规范。关键的新奇是一个类型导向的概念，可见的诱导性，这确保了算法朝着它的目标，因为它之间交替削弱和加强候选不变。该算法是参数化的基于示例的合成引擎和验证器，我们证明了它是健全的和完整的有限类型的一阶模块，假设合成器和验证器以及。我们实现了这些想法在一个工具称为河内，它合成递归数据类型的表示不变量。河内不仅处理一阶代码的不变量，还处理高阶代码的不变量。在后端，河内使用一个名为Myth的枚举合成器和一个枚举测试工具作为验证器。由于河内使用测试进行验证，所以它并不可靠，尽管我们的经验评估表明，它在我们调查的基准上是成功的。
A representation invariant is a property that holds of all values of abstract type produced by a module. Representation invariants play important roles in software engineering and program verification. In this paper, we develop a counterexample-driven algorithm for inferring a representation invariant that is sufficient to imply a desired specification for a module. The key novelty is a type-directed notion of visible inductiveness, which ensures that the algorithm makes progress toward its goal as it alternates between weakening and strengthening candidate invariants. The algorithm is parameterized by an example-based synthesis engine and a verifier, and we prove that it is sound and complete for first-order modules over finite types, assuming that the synthesizer and verifier are as well. We implement these ideas in a tool called Hanoi, which synthesizes representation invariants for recursive data types. Hanoi not only handles invariants for first-order code, but higher-order code as well. In its back end, Hanoi uses an enumerative synthesizer called Myth and an enumerative testing tool as a verifier. Because Hanoi uses testing for verification, it is not sound, though our empirical evaluation shows that it is successful on the benchmarks we investigated.
登录
查看更多内容
SLING：使用动态分析来推断分离逻辑中的程序不变量
DOI：
10.1145/3314221.3314634
发表时间：
2019
期刊：
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
T. Le;Guolong Zheng;Thanhvu Nguyen
通讯作者：
Thanhvu Nguyen
Artifact 的复制包：数据驱动的表示不变量推理
DOI：
--
发表时间：
2020
期刊：
影响因子：
--
作者：
Anders Miltner;Saswat Padhi;T. Millstein;David Walker
通讯作者：
David Walker
DOI：
--
发表时间：
2019
期刊：
arXiv.org
影响因子：
--
作者：
Lau Skorstengaard
通讯作者：
Lau Skorstengaard
ELDARICA 号角求解器
DOI：
--
发表时间：
2018
期刊：
Formal Methods in Computer-Aided Design
影响因子：
--
作者：
Hossein Hojjat;P. Rümmer
通讯作者：
P. Rümmer
第 37 届 ACM SIGPLAN 编程语言设计与实现会议论文集
DOI：
--
发表时间：
2016
期刊：
ACM-SIGPLAN Symposium on Programming Language Design and Implementation
影响因子：
--
作者：
C. Krintz;E. Berger
通讯作者：
E. Berger