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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Balakrishnan, G., Reps, T., Kidd, N., Lal, A., Lim, J., Melski, D., … Teitelbaum, T. (2005). Model checking x86 executables with CodeSurfer/x86 and WPDS++. In Lecture Notes in Computer Science (Vol. 3576, pp. 158–163). Springer Verlag. https://doi.org/10.1007/11513988_17
Mendeley helps you to discover research relevant for your work.