Adding Constraint Building Mechanisms to a Symbolic Execution Engine Developed for Detecting Runtime Errors

Abstract

Most of the runtime failures of a software system can be revealed during test execution only, which has a very high cost. The symbolic execution engine developed at the Software Engineering Department of University of Szeged is able to detect runtime errors (such as null pointer dereference, bad array indexing, division by zero) in Java programs without running the program in real-life environment.

In this paper we present a constraint system building mechanism which improves the accuracy of the runtime errors found by the symbolic execution engine mentioned above. We extend the original principles of symbolic execution by tracking the dependencies of the symbolic variables and substituting them with concrete values if the built constraint system unambiguously determines their value.

The extended symbolic execution checker was tested on real-life open-source systems as well.

@InProceedings{KHF15,
    author    = {K\'ad\'ar, Istv\'an and Heged\H{u}s, P\'eter and Ferenc, Rudolf},
    booktitle = {Proceedings of the 15th International Conference on Computational Science and Its Applications (ICCSA 2015)},
    title     = {Adding Constraint Building Mechanisms to a Symbolic Execution Engine Developed for Detecting Runtime Errors},
    year      = {2015},
    address   = {Banff, Alberta, Canada},
    month     = jun,
    pages     = {20--35},
    publisher = {Springer-Verlag},
    series    = {Lecture Notes in Computer Science (LNCS)},
    volume    = {9159},
    doi       = {10.1007/978-3-319-21413-9_2},
    keywords  = {Software engineering, Symbolic execution, Java runtime errors, Constraint system building},
    url       = {https://link.springer.com/chapter/10.1007%2F978-3-319-21413-9_2},
}