Model checking x86 executables with Codesurfer/x86 and WPDS++
Gogul Balakrishnan, Thomas Reps, Nicholas Kidd, Akash Lal, Junghee Lim, David Melski, Radu Gruian, Suan Yong, Chi-Hua Chen, and Tim Teitelbaum.
In 17th International Conference on Computer Aided Verification (CAV).
Edinburgh, Scotland, July 2005.
This paper presents a toolset for model checking x86 executables. The members of the toolset are CodeSurfer/x86, WPDS++, and the Path Inspector. CodeSurfer/x86 is used to extract a model from an executable in the form of a weighted pushdown system. WPDS++ is a library for answering generalized reachability queries on weighted pushdown systems. The Path Inspector is a software model checker built on top of CodeSurfer and WPDS++ that supports safety queries about the program's possible control configurations.
