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.

Publications

Software

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