Counterexample-guided focus
Counterexample-guided focus
复制标题
反例引导焦点
DOI：
10.1145/1706299.1706330
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
T. Wies
中科院分区：
文献类型：
--
作者：
A. Podelski;T. Wies
量化不变量的自动推理被认为是软件验证的下一个挑战之一。在这里，对于相应的程序分析来说，正确的精度-效率权衡的问题归结为正确处理全称量词上下的析取的问题。在形状分析的密切相关的设置中，使用焦点运算符，以使析取的处理（以及效率-精度的权衡）适应于单个程序语句。一个很有前途的研究方向是设计参数化版本的焦点运营商，允许用户微调的焦点运营商不仅对个别程序语句，但也对特定的验证任务。我们把这个研究方向再向前推进一步。我们针对分析的每一步（针对特定的验证任务）微调焦点操作符。这种微调必须自动完成。我们的想法是使用反例来达到这个目的。我们实现了这个想法的工具，自动推断量化的不变量的各种堆操作程序的验证。
The automated inference of quantified invariants is considered one of the next challenges in software verification. The question of the right precision-efficiency tradeoff for the corresponding program analyses here boils down to the question of the right treatment of disjunction below and above the universal quantifier. In the closely related setting of shape analysis one uses the focus operator in order to adapt the treatment of disjunction (and thus the efficiency-precision tradeoff) to the individual program statement. One promising research direction is to design parameterized versions of the focus operator which allow the user to fine-tune the focus operator not only to the individual program statements but also to the specific verification task. We carry this research direction one step further. We fine-tune the focus operator to each individual step of the analysis (for a specific verification task). This fine-tuning must be done automatically. Our idea is to use counterexamples for this purpose. We realize this idea in a tool that automatically infers quantified invariants for the verification of a variety of heap-manipulating programs.
登录
查看更多内容
通过归纳学习进行抽象细化
DOI：
10.1007/11513988_50
发表时间：
2005
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
Alexey Loginov;T. Reps;Shmuel Sagiv
通讯作者：
Shmuel Sagiv
通过抽象解释进行形式语言、语法和基于集合约束的程序分析
DOI：
10.1145/224164.224199
发表时间：
1995
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
P. Cousot;R. Cousot
通讯作者：
R. Cousot
布尔堆
影响因子：
8.7
作者：
A. Podelski;Thomas Wies
通讯作者：
Thomas Wies
DOI：
10.1145/1749608.1749613
发表时间：
2003
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
T. Reps;Shmuel Sagiv;Alexey Loginov
通讯作者：
Alexey Loginov
Hob：验证数据结构一致性的工具
DOI：
10.1007/978-3-540-31985-6_16
发表时间：
2005
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
Patrick Lam;Viktor Kunčak;M. Rinard
通讯作者：
M. Rinard