Abstracting Path Conditions

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

STREJČEK Jan TRTÍK Marek

Year of publication 2012
Type Article in Proceedings
Conference Proceedings of the 2012 International Symposium on Software Testing and Analysis, ISSTA 2012
MU Faculty or unit

Faculty of Informatics

Citation
Web http://doi.acm.org/10.1145/2338965.2336772
Doi http://dx.doi.org/10.1145/2338965.2336772
Field Informatics
Keywords Symbolic execution; Path conditions; Program location reachability; Tests generation
Description We present a symbolic-execution-based algorithm that for a given program and a given program location in it produces a nontrivial necessary condition on input values to drive the program execution to the given location. The algorithm is based on computation of loop summaries for loops along acyclic paths leading to the target location. We also propose an application of necessary conditions in contemporary bug-finding and test-generation tools. Experimental results on several small benchmarks show that the presented technique can in some cases significantly improve performance of the tools.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.