Una Revisión sobre la Ejecución Simbólica de Programas Computacionales

El objetivo de este articulo es presentar la ejecucion simbolica de programas y su extension, ejecucion simbolica generalizada, para senalar las mejoras necesarias a la ejecucion simbolica para que llegue a ser un enfoque practico de verificacion de programas. El analisis de programas permite determinar niveles de correctitud de software o cumplimiento de los requerimientos de usuario. Existen dos enfoques para la verificacion de programas, analitica y dinamica, y en medio de ellas, existe la ejecucion simbolica la que estaticamente analiza el codigo fuente de programas, y dinamicamente simula la ejecucion de las instrucciones ejecutables de programas por medio de datos de entrada simbolicos. En este trabajo se describe los conceptos de verificacion de programas, la propuesta original de ejecucion simbolica junto a sus ventajas y desventajas, y las principales caracteristicas de ejecucion simbolica generalizada. Finalmente, se resumen las principales areas de investigacion que se abren relacionadas con la ejecucion simbolica.