一句话：提出 VeriAbs，一个面向 C 程序的可达性验证器，按循环类型选择由抽象、模型检测与测试生成等技术组成的策略组合。
程序验证仍具挑战，单一技术无法在所有程序上成功。VeriAbs 是面向 C 程序的可达性验证器，采用技术组合（portfolio）思路，将多种验证技术组织为四种策略，每种策略按特定顺序应用若干技术，并根据程序中循环的类型选择策略。其技术包括显式状态模型检测、有界模型检测、抽象与测试生成等。作者在 SV-COMP 2019 ReachSafety 类别的 3831 个验证任务上评估了各策略的有效性，发现经典技术虽能解决多数程序，但剩余程序需要广泛结合更多技术。该工作展示了按循环特征动态编排验证技术组合的可行性与必要性。
Verification of programs continues to be a challenge and no single known technique succeeds on all programs. In this paper we present VeriAbs, a reachability verifier for C programs that incorporates a portfolio of techniques implemented as four strategies, where each strategy is a set of techniques applied in a specific sequence. It selects a strategy based on the kind of loops in the program. We analysed the effectiveness of the implemented strategies on the 3831 verification tasks from the ReachSafety category of the 8th International Competition on Software Verification (SV-COMP) 2019 and found that although classic techniques - explicit state model checking and bounded model checking, succeed on a majority of the programs, a wide range of further techniques are required to analyse the rest. A screencast of the tool is available at https://youtu.be/Hzh3PPiODwk.
DOI 原文 ·
@inproceedings{paperbot5277,
title = {VeriAbs : Verification by Abstraction and Test Generation},
author = {Mohammad Afzal and A. Asia and Avriti Chauhan and Bharti Chimdyalwar and Priyanka Darke and Advaita Datar and Shrawan Kumar and R. Venkatesh},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00121}
}