一句话：提出符号正则验证 SRV，通过路径切片与引导缓解路径爆炸，高效验证程序的正则性质。
验证程序的正则性质长期具有挑战性。本文提出符号正则验证（SRV），基于动态符号执行（DSE），并引入两项缓解路径爆炸的新技术：面向正则性质的路径切片，以及路径切片与引导的协同结合；切片剪除冗余路径，引导增强反例搜索。作者为 Java 实现 SRV，在 15 个真实开源 Java 程序（共 259K 行）上评估。相比纯 DSE、纯引导和纯路径切片等先进方法，SRV 平均加速分别超过 8.4X、8.6X、7X，使符号正则性质验证显著更实用。
Verifying the regular properties of programs has been a significant challenge. This paper tackles this challenge by presenting symbolic regular verification (SRV) that offers significant speedups over the state-of-the-art. SRV is based on dynamic symbolic execution (DSE) and enabled by novel techniques for mitigating path explosion: (1) a regular property-oriented path slicing algorithm, and (2) a synergistic combination of property-oriented path slicing and guiding. Slicing prunes redundant paths, while guiding boosts the search for counterexamples. We have implemented SRV for Java and evaluated it on 15 real-world open-source Java programs (totaling 259K lines of code). Our evaluation results demonstrate the effectiveness and efficiency of SRV. Compared with the state-of-the-art --- pure DSE, pure guiding, and pure path slicing --- SRV achieves average speedups of more than 8.4X, 8.6X, and 7X, respectively, making symbolic regular property verification significantly more practical.
DOI 原文 ·
@inproceedings{paperbot4467,
title = {Symbolic verification of regular properties},
author = {Hengbiao Yu and Zhenbang Chen and Ji Wang and Zhendong Su and Wei Dong},
booktitle = {ICSE},
year = {2018},
doi = {10.1145/3180155.3180227}
}