A review about symbolic execution of computer programs

被引：0

作者：

Vidal, Cristian L. ^{[1
]}

Schmal, Rodolfo F. ^{[2
]}

Rivero, Sabino ^{[2
]}

Villarroel, Rodolfo H. ^{[3
]}

机构：

[1] Escuela de Ingeniería Informática, Facultad de Ingeniería y Administración, Universidad Bernardo O'Higgins, Santiago, Avenida Viel 1497

[2] Escuela de Ingeniería Informática Empresarial, Facultad de Ciencias Empresariales, Universidad de Talca Campus Lircay, Talca, Avenida Lircay S/N

[3] Escuela de Ingeniería Informática, Facultad de Ingeniería, Pontificia Universidad Católica de Valparaíso, Valparaíso

来源：

Informacion Tecnologica | 2014年 / 25卷 / 03期

关键词：

GSE; Software verification; Symbolic execution; SymExe;

D O I：

10.4067/S0718-07642014000300014

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：115 / 124

页数：9

共 15 条

[1]

Baier C., Katoen J., Principles of Model Checking (Representation and Mind Series), (2008)

[2]

Belt J., Et al., Bakar, Kiasan: Flexible contract checking for critical systems using symbolic execution, Actas de Third International Conference on NASA Formal Methods, NFM'11, pp. 58-72, (2011)

[3]

Cadar C., Et al., Symbolic execution for software testing in practice: Preliminary assessment, Actas de 3rd International Conference on Software Engineering, ICSE '11, pp. 1066-1071, (2011)

[4]

Cadar C., Sen K., Symbolic execution for software testing: Three decades later, Comunicaciones de la ACM, 56, 2, pp. 82-90, (2013)

[5]

Dijkstra E.W., The humble programmer, Comunicaciones de la ACM, 15, 10, pp. 859-866, (1972)

[6]

Ghezzi C., Jazayeri M., Mandrioli D., Fundamentals of Software Engineering, SegundaEdición, (2002)

[7]

Holzmann G.J., Software analysis, model checking, Actas de 14th International Conference on Computer Aided Verification, CAV '02, pp. 1-16, (2002)

[8]

Java Pathfinder the Swiss Army Knife of Java Verification

[9]

Khurshid S., Pasareanu C., Visser W., Generalized symbolic execution for model checking and testing, Actas de 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'03, pp. 553-568, (2003)

[10]

King J.C., Symbolic execution, program testing, Comunicaciones de la ACM, 19, 7, pp. 385-394, (1976)

← 1 2 →