StaDy: Deep Integration of Static and Dynamic Analysis in Frama-CReport as inadecuate




StaDy: Deep Integration of Static and Dynamic Analysis in Frama-C - Download this document for free, or read online. Document in PDF available to download.

1 LSL - Laboratoire Sûreté des Logiciels LIST - Laboratoire d-Intégration des Systèmes et des Technologies : DRT-LIST 2 CASSIS - Combination of approaches to the security of infinite states systems FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods 3 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies

Abstract : We present StaDy, a new integration of the concolic test generator PathCrawler within the software analysis platform Frama- C. When executing a dynamic analysis of a C code, the integrated test generator also exploits its formal specification, written in an executable fragment of the acsl specification language shared with other analyzers of Frama-C. The test generator provides the user with accurate verdicts, that other Frama-C plugins can reuse to improve their own analyses. This tool is designed to be the foundation stone of static and dynamic analysis combinations in the Frama-C platform. Our first experiments confirm the benefits of such a deep integration of static and dynamic analysis within the same platform.





Author: Guillaume Petiot - Nikolai Kosmatov - Alain Giorgetti - Jacques Julliand -

Source: https://hal.archives-ouvertes.fr/



DOWNLOAD PDF




Related documents