Skip to main content

Guiding Dynamic Symbolic Execution Toward Unverified Program Executions

Christakis, Maria and Müller, Peter and Wüstholz, Valentin (2016) Guiding Dynamic Symbolic Execution Toward Unverified Program Executions. In: Proceedings of the 38th International Conference on Software Engineering. ICSE International Conference on Software Engineering . ACM, New York, USA, pp. 144-155. ISBN 978-1-4503-3900-1. (doi:10.1145/2884781.2884843)

Abstract

Most techniques to detect program errors, such as testing, code reviews, and static program analysis, do not fully verify all possible executions of a program. They leave executions unverified when they do not check certain properties, fail to verify properties, or check properties under certain unsound assumptions such as the absence of arithmetic overflow.

In this paper, we present a technique to complement partial verification results by automatic test case generation. In contrast to existing work, our technique supports the common case that the verification results are based on unsound assumptions. We annotate programs to reflect which executions have been verified, and under which assumptions. These annotations are then used to guide dynamic symbolic execution toward unverified program executions. Our main technical contribution is a code instrumentation that causes dynamic symbolic execution to abort tests that lead to verified executions, to prune parts of the search space, and to prioritize tests that cover more properties that are not fully verified. We have implemented our technique for the .NET static analyzer Clousot and the dynamic symbolic execution tool Pex. It produces smaller test suites (by up to 19.2%), covers more unverified executions (by up to 7.1%), and reduces testing time (by up to 52.4%) compared to combining Clousot and Pex without our technique.

Item Type: Book section
DOI/Identification number: 10.1145/2884781.2884843
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: M. Christaki
Date Deposited: 23 Nov 2016 14:53 UTC
Last Modified: 24 Sep 2019 07:57 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/58937 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year