Distributed CFG-based symbolic execution for assembly programs

Symbolic execution is one of the effective dynamic verification methods and there are some researches on application of it to assembly programs. However, symbolic execution has well-known problems: First, symbolic execution can't deal with some programs with containing loops. Second, symbolic execution sometimes causes the path explosion. In particular, assembly programs more often suffer from these problems because of its characteristic control flow such as interruptions. In this paper, we propose the Distributed CFG(Control Flow Graph)-based Symbolic Execution to solve these problems.