Backward Symbolic Execution with Loop Folding

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F21%3A00122663" target="_blank" >RIV/00216224:14330/21:00122663 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007%2F978-3-030-88806-0_3" target="_blank" >https://link.springer.com/chapter/10.1007%2F978-3-030-88806-0_3</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-88806-0_3" target="_blank" >10.1007/978-3-030-88806-0_3</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Backward Symbolic Execution with Loop Folding

Popis výsledku v původním jazyce

Symbolic execution is an established program analysis tech- nique that aims to search all possible execution paths of the given pro- gram. Due to the so-called path explosion problem, symbolic execution is usually unable to analyze all execution paths and thus it is not convenient for program verification as a standalone method. This paper focuses on backward symbolic execution (BSE), which searches program paths backwards from the error location whose reachability should be proven or refuted. We show that this technique is equivalent to performing k-induction on control-flow paths. While standard BSE simply unwinds all program loops, we present an extension called loop folding that aims to derive loop invariants during BSE that are sufficient to prove the unreachability of the error location. The resulting technique is called backward symbolic execution with loop folding (BSELF). Our experiments show that BSELF performs better than BSE and other tools based on k-induction when non-trivial benchmarks are considered. Moreover, a sequential combination of symbolic execution and BSELF achieved very competitive results compared to state-of-the-art verification tools.

Název v anglickém jazyce

Backward Symbolic Execution with Loop Folding

Popis výsledku anglicky

Symbolic execution is an established program analysis tech- nique that aims to search all possible execution paths of the given pro- gram. Due to the so-called path explosion problem, symbolic execution is usually unable to analyze all execution paths and thus it is not convenient for program verification as a standalone method. This paper focuses on backward symbolic execution (BSE), which searches program paths backwards from the error location whose reachability should be proven or refuted. We show that this technique is equivalent to performing k-induction on control-flow paths. While standard BSE simply unwinds all program loops, we present an extension called loop folding that aims to derive loop invariants during BSE that are sufficient to prove the unreachability of the error location. The resulting technique is called backward symbolic execution with loop folding (BSELF). Our experiments show that BSELF performs better than BSE and other tools based on k-induction when non-trivial benchmarks are considered. Moreover, a sequential combination of symbolic execution and BSELF achieved very competitive results compared to state-of-the-art verification tools.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings

ISBN

9783030888053

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

28

Strana od-do

49-76

Název nakladatele

Springer

Místo vydání

Cham (Switzerland)

Místo konání akce

Chicago

Datum konání akce

1. 1. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000720084200003