* ICSE 2018 *
Sun 27 May - Sun 3 June 2018 Gothenburg, Sweden
Fri 1 Jun 2018 11:20 - 11:40 at Congress Hall - Testing III Chair(s): Myra Cohen

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.

Fri 1 Jun

11:00 - 12:30: Technical Papers - Testing III at Congress Hall
Chair(s): Myra CohenUniversity of Nebraska-Lincoln
icse-2018-Technical-Papers152784360000011:00 - 11:20
DOI File Attached
icse-2018-Technical-Papers152784480000011:20 - 11:40
Research paper
Hengbiao Yu, Zhenbang ChenCollege of Computer, National University of Defense Technology, Ji Wang, Zhendong SuUniversity of California, Davis, Wei Dong
icse-2018-Journal-first-papers152784600000011:40 - 12:00
icse-2018-Journal-first-papers152784720000012:00 - 12:20
Narayan RamasubbuUniversity of Pittsburgh, USA , Chris KemererUniversity of Pittsburgh
icse-2018-Technical-Papers152784840000012:20 - 12:30