Trigger Selection Strategies to Stabilize Program Verifiers
Trigger Selection Strategies to Stabilize Program Verifiers
复制标题
触发选择策略以稳定程序验证者
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Clément Pit
中科院分区：
文献类型：
--
作者：
K. Leino;Clément Pit
基于SMT的程序验证者通常会遭受所谓的蝴蝶效应，其中对程序源的较小修改在验证时间中引起了重要的不稳定性，这又可能导致虚假的验证失败和降级的用户体验。 （行为不良的量化器，导致SMT求解器反复实例化一组量化的公式）作为这些不稳定性的重要贡献者，并描述了某些技术以检测和预防其核心。从SMT求解器到高级验证者：此举允许验证者的作者注释，重写和分析用户编写的量词以改善求解器的性能，使用易于在源级别获得的信息，但很难从求解器使用的重量编码术语中提取。 DAFNY的测试套件和使用DAFNY的大量验证工作。
SMT-based program verifiers often suffer from the so-called butterfly effect, in which minor modifications to the program source cause significant instabilities in verification times, which in turn may lead to spurious verification failures and a degraded user experience. This paper identifies matching loops (ill-behaved quantifiers causing an SMT solver to repeatedly instantiate a small set of quantified formulas) as a significant contributor to these instabilities, and describes some techniques to detect and prevent them. At their core, the contributed techniques move the trigger selection logic away from the SMT solver and into the high-level verifier: this move allows authors of verifiers to annotate, rewrite, and analyze user-written quantifiers to improve the solver’s performance, using information that is easily available at the source level but would be hard to extract from the heavily encoded terms that the solver works with. The paper demonstrates three core techniques (quantifier splitting, trigger sharing, and matching loop detection) by extending the Dafny verifier with its own trigger selection routine, and demonstrates significant predictability and performance gains on both Dafny’s test suite and large verification efforts using Dafny.