OSMOSE: automatic structural testing of executables. Verification is usually performed on a high-level view of the software, either specification or program source code. However, in certain circumstances verification is more relevant when performed at the machine-code level. This paper focuses on automatic test data generation from a stand-alone executable. Low-level analysis is much more difficult than high-level analysis since even the control-flow graph is not available and bit-level instructions have to be modelled faithfully. The paper shows how ‘path-based’ structural test data generation can be adapted from structured language to machine code, using both state-of-the-art technologies and innovative techniques. The results have been implemented in a tool named OSMOSE and encouraging experiments have been conducted.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 5 articles , 1 standard article )

Showing results 1 to 5 of 5.
Sorted by year (citations)

  1. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  2. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  3. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2012)
  4. Bardin, Sébastien; Herrmann, Philippe: OSMOSE: automatic structural testing of executables (2011) ioport
  5. Bardin, Sébastien; Herrmann, Philippe; Védrine, Franck: Refinement-based CFG reconstruction from unstructured programs (2011)