Balakrishnan, G.; Reps, T.; Kidd, N.; Lal, A.; Lim, J.; Melski, D.; Gruian, R.; Yong, S.; Chen, C.-H.; Teitelbaum, T. Model checking x86 executables with CodeSurfer/x86 and WPDS++. (English) Zbl 1081.68604 Etessami, Kousha (ed.) et al., Computer aided verification. 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27231-3/pbk). Lecture Notes in Computer Science 3576, 158-163 (2005). Summary: 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.For the entire collection see [Zbl 1078.68004]. Cited in 4 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) Software:CodeSurfer; StEAM; TVOC; veriSoft; WPDS++ PDF BibTeX XML Cite \textit{G. Balakrishnan} et al., Lect. Notes Comput. Sci. 3576, 158--163 (2005; Zbl 1081.68604) Full Text: DOI