El objetivo de este artículo es presentar la ejecución simbólica de programas y su extensión, ejecución simbólica generalizada, para señalar las mejoras necesarias a la ejecución simbólica para que llegue a ser un enfoque práctico de verificación de programas. El análisis de programas permite determinar niveles de correctitud de software o cumplimiento de los requerimientos de usuario. Existen dos enfoques para la verificación de programas, analítica y dinámica, y en medio de ellas, existe la ejecución simbólica la que estáticamente analiza el código fuente de programas, y dinámicamente simula la ejecución de las instrucciones ejecutables de programas por medio de datos de entrada simbólicos. En este trabajo se describe los conceptos de verificación de programas, la propuesta original de ejecución simbólica junto a sus ventajas y desventajas, y las principales características de ejecución simbólica generalizada. Finalmente, se resumen las principales áreas de investigación que se abren relacionadas con la ejecución simbólica.

The objective of this paper is to present the symbolic execution of programs and its extension, generalized symbolic execution, to indicate the necessary improvements to symbolic execution so that it becomes a practical approach for program verification. Program analysis allows determining levels of software correctness or compliance with the user requirements. There are two approaches for program verification, analytic and dynamic, and, between them, symbolic execution exits which statically analyzes the program source code, and dynamically simulates the execution of executable instructions of programs by means of symbolic input data. In this paper, concepts of program verification, the original proposal of symbolic execution along with their advantages and disadvantages, and the main features of generalized symbolic execution are described. Finally, the main open research areas related to symbolic execution are summarized.