Symbolic execution formally explained

被引：7

作者：

de Boer, Frank S. ^{[1
,2
]}

Bonsangue, Marcello ^{[2
]}

机构：

[1] Ctr Wiskunde & Informat CWI, Leiden, Netherlands

[2] Leiden Univ, Leiden Inst Adv Comp Sci LIACS, Leiden, Netherlands

来源：

FORMAL ASPECTS OF COMPUTING | 2021年 / 33卷 / 4-5期

关键词：

D O I：

10.1007/s00165-020-00527-y

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

In this paper, we provide a formal explanation of symbolic execution in terms of a symbolic transition system and prove its correctness and completeness with respect to an operational semantics which models the execution on concrete values.We first introduce a formalmodel for a basic programming languagewith a statically fixed number of programming variables. This model is extended to a programming language with recursive procedures which are called by a call-by-value parameter mechanism. Finally, we present a more general formal framework for proving the soundness and completeness of the symbolic execution of a basic object-oriented language which features dynamically allocated variables.

引用

页码：617 / 636

页数：20

共 26 条

[1]

Albert Elvira, 2014, Formal Methods for Executable Software Models. 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014. Advanced Lectures: LNCS 8483, P263, DOI 10.1007/978-3-319-07317-0_7

[2]

Andrei, 2017, J SYMB COMPUT, V80, P125

[3]

[Anonymous], 2008, P OSDI

[4]

Apt Krzysztof, 2009, VERIFICATION SEQUENT

[5]

Boer Frank S., 2019, Formal Methods - The Next 30 Years. Third World Congress, FM 2019. Proceedings. Lecture Notes in Computer Science (LNCS 11800), P64, DOI 10.1007/978-3-030-30942-8_6

[6]

Bonsangue M. M., 1994, Formal Aspects of Computing, V6, P788, DOI 10.1007/BF01213603

[7] Symbolic Execution of Programs with Heap Inputs [J].

Braione, Pietro ;

Denaro, Giovanni ;

Pezze, Mauro .

2015 10TH JOINT MEETING OF THE EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND THE ACM SIGSOFT SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (ESEC/FSE 2015) PROCEEDINGS, 2015, :602-613

[8] Snugglebug: A Powerful Approach To Weakest Preconditions [J].

Chandra, Satish ;

Fink, Stephen J. ;

Sridharan, Manu .

ACM SIGPLAN NOTICES, 2009, 44 (06) :363-374

[9]

CRISTIAN C, 2008, ACM T INFORM SYST SE, V12

[10]

David, 1981, TEXTS MONOGRAPHS COM

← 1 2 3 →