Abstract
In order to prevent, detect and fix errors in software, various code analysis techniques have been developed and are practically used, e.g. abstract interpretation or concolic execution. We want to bring into attention backward symbolic execution, a technique not widely used despite its advantages such as a demand-driven approach.
We synthesize its current state-of-the-art into an algorithm extensible by various heuristics. This algorithm is then implemented and evaluated on a set of example programs which contain both valid and invalid assertions to be verified and refuted.
According to the results, backward symbolic execution can successfully complement both abstract interpretation and concolic execution to achieve significantly higher success rate.