Abstracting Path Conditions

Jan Strejček, Marek Trtík

We present a symbolic-execution-based algorithm that for a given program and a given program location produces a nontrivial necessary condition on input values to drive the program execution to the given location. We also propose an application of necessary conditions in contemporary bug-finding and test-generation tools. Experimental results show that the presented technique can significantly improve performance of the tools.

Knowledge Graph



Sign up or login to leave a comment