StaDy: Deep Integration of Static and Dynamic Analysis in Frama-CReportar como inadecuado




StaDy: Deep Integration of Static and Dynamic Analysis in Frama-C - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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.





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

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



DESCARGAR PDF




Documentos relacionados