一句话：提出基于 reducer 的构造方法，将现有验证器改造成能够接收并利用条件的条件验证器。
论文关注软件验证中单一验证器难以完成困难任务的问题，主张联合多种采用不同技术的验证器，并通过条件模型检查在验证器之间交换信息：第一个验证器输出一个条件，描述其已成功验证的状态空间，第二个验证器据此只验证尚未验证的部分。然而多数验证器并不支持把条件作为输入。为此，论文提出基于 reducer 的构造方法，用以将现有验证器改造成条件验证器，从而能够理解并利用前序验证器产生的条件。摘要未给出具体实验评估与结果。
Despite recent advances, software verification remains challenging. To solve hard verification tasks, we need to leverage not just one but several different verifiers employing different technologies. To this end, we need to exchange information between verifiers. Conditional model checking was proposed as a solution to exactly this problem: The idea is to let the first verifier output a condition which describes the state space that it successfully verified and to instruct the second verifier to verify the yet unverified state space using this condition. However, most verifiers do not understand conditions as input.
DOI 原文 ·
@inproceedings{paperbot4463,
title = {Reducer-based construction of conditional verifiers},
author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger and Heike Wehrheim},
booktitle = {ICSE},
year = {2018},
doi = {10.1145/3180155.3180259}
}