Conflict-Driven Symbolic Execution (CDSE) is a novel algorithm that I introduced
during my MSc thesis that tackles the path explosion problem faced by symbolic
execution. This algorithm can dynamically reduce the number of paths explored
during symbolic execution in order to prove a given set of properties. The
algorithm is capable of learning from conflicts detected while symbolically
executing a path.
CDSE was inspired by the conflict-driven clause learning (CDCL) insights
introduced by modern boolean satisfiability solvers. It
takes advantage of two features responsible for the success of CDCL solvers:
conflict analysis and non-chronological backtracking. In a nutshell, CDSE prunes
the search space every time a certain branch is proven infeasible, by learning
the reason why there is a conflict.
Kite is a proof-of-concept tool that I developed to assess this new algorithm.
The results I found so far are encouraging (check my thesis), and they represent practical evidence that
conflict-driven symbolic execution can perform better than regular symbolic
execution.
Please send any questions, concerns or comments to Celina Val. I would really appreciate if you put a tag "[Kite]" in the email subject. =D