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 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30 | Testing IIIJournal first papers / Technical Papers at Congress Hall Chair(s): Myra Cohen University of Nebraska-Lincoln | ||
11:00 20mTalk | RFC-Directed Differential Testing of Certificate Validation in SSL/TLS Implementations Technical Papers DOI File Attached | ||
11:20 20mResearch paper | Symbolic Verification of Regular Properties Technical Papers Hengbiao Yu , Zhenbang Chen College of Computer, National University of Defense Technology, Ji Wang , Zhendong Su University of California, Davis, Wei Dong Pre-print | ||
11:40 20mTalk | Metamorphic Testing of RESTful Web APIs Journal first papers Sergio Segura , José Antonio Parejo Maestre University of Sevilla, Javier Troya , Antonio Ruiz-Cortés Universidad de Sevilla | ||
12:00 20mTalk | Integrating Technical Debt Management and Software Quality Management Processes: A Normative Framework and Field Tests Journal first papers | ||
12:20 10mTalk | Q&A in groups Technical Papers |