Ejecución simbólica como herramienta de análisis

Abstract

[ES] El análisis automático de software permite verificar que un programa cumpla una serie de propiedades deseables sin intervención humana, aportando agilidad al proceso de ingeniería y reduciendo los riesgos del software crítico. No obstante, para analizar un programa mediante un computador se requiere conocer las especificaciones formales a evaluar, no siempre al alcance del desarrollador. En este trabajo se elabora la base tecnológica de un sistema para inferir especificaciones automáticamente, aplicando ejecución simbólica sobre la semántica de un lenguaje derivado de C y facilitando así el proceso de verificación.

[EN] Automatic software analysis allows developers to verify if a program satisfies a series of desirable properties without human intervention, accelerating the engineering process and reducing the risks of critical software. However, in order to perform the analysis of a program, its formal specifications are required to be known, and usually it is too difficult to produce them manually. In this paper we elaborate the technological basis for a system that performs automatic inference of specifications, applying symbolic execution over the semantics of a derivative language of C so that we can make easier the verification process.