zbMATH — the first resource for mathematics

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].

68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI