Una revisión sobre la ejecución simbólica de programas computacionales

Abstract

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.