一句话：提出基于SMT的多阶段循环蕴含不变式合成方法，可同时发现相互依赖的周期性阶段不变式。
多阶段循环因需要析取式不变式而难以验证；其中一类不变式可表示为阶段前置条件与阶段内有效引理之间的蕴含关系，但现有先进验证器对此类不变式结构支持不足。本文提出一种基于SMT的蕴含不变式合成方法：利用模型投影（Model Based Projections）发现程序阶段，并结合数据学习推断循环变量在任意位置的关联。该方法能够处理相互依赖的周期阶段，此类场景需要同时发现多个蕴含不变式。作者实现了该算法并与多个先进求解器进行对比，在具有复杂阶段结构的程序上展现出有前景的验证效果。
Loops with multiple phases are challenging to verify because they require disjunctive invariants. Invariants could also have the form of implication between a precondition for the phase and a lemma that is valid throughout the phase. Such invariant structure is however not widely supported in state-of-the-art verification. We present a novel SMT-based approach to synthesize implication invariants for multi-phase loops. Our technique computes Model Based Projections to discover the program's phases and leverages data learning to get relationships among loop variables at an arbitrary place in the loop. It is effective in the challenging cases of mutually-dependent periodic phases, where many implication invariants need to be discovered simultaneously. Our approach has shown promising results in its ability to verify programs with complex phase structures. We have implemented and evaluated our algorithm against several state-of-the-art solvers.
DOI 原文 ·
@inproceedings{paperbot7130,
title = {Multi-phase invariant synthesis},
author = {Daniel Riley and Grigory Fedyukovich},
booktitle = {FSE},
year = {2022},
doi = {10.1145/3540250.3549166}
}