Backward Symbolic Execution with Loop Folding

D 2021

Backward Symbolic Execution with Loop Folding

CHALUPA, Marek a Jan STREJČEK

Základní údaje

Originální název

Backward Symbolic Execution with Loop Folding

Autoři

CHALUPA, Marek (203 Česká republika, garant, domácí) a Jan STREJČEK (203 Česká republika, domácí)

Vydání

Cham (Switzerland), Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings, od s. 49-76, 28 s. 2021

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/21:00122663

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-88805-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-88806-0_3

UT WoS

000720084200003

Klíčová slova anglicky

symbolic execution;k-induction;backward symbolic execution;inductive invariants;invariants

Štítky

core_B, firank_B, formal verification, formela-ver, program analysis, Symbiotic

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 23. 5. 2022 15:01, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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ávaznosti

MUNI/A/1108/2020, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X. (Akronym: SV-FI MAV X.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X.

MUNI/A/1549/2020, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21 (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21

Citovat

CHALUPA, Marek a Jan STREJČEK. Backward Symbolic Execution with Loop Folding. Online. In Cezara Dragoi, Suvam Mukherjee, and Kedar S. Namjoshi. Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings. Cham (Switzerland): Springer, 2021, s. 49-76. ISBN 978-3-030-88805-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-88806-0_3.

@inproceedings{1799589,
   author = {Chalupa, Marek and Strejček, Jan},
   address = {Cham (Switzerland)},
   booktitle = {Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-030-88806-0_3},
   editor = {Cezara Dragoi, Suvam Mukherjee, and Kedar S. Namjoshi},
   keywords = {symbolic execution;k-induction;backward symbolic execution;inductive invariants;invariants},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-030-88805-3},
   pages = {49-76},
   publisher = {Springer},
   title = {Backward Symbolic Execution with Loop Folding},
   url = {https://link.springer.com/chapter/10.1007%2F978-3-030-88806-0_3},
   year = {2021}
}

TY  - JOUR
ID  - 1799589
AU  - Chalupa, Marek - Strejček, Jan
PY  - 2021
TI  - Backward Symbolic Execution with Loop Folding
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783030888053
KW  - symbolic execution;k-induction;backward symbolic execution;inductive invariants;invariants
UR  - https://link.springer.com/chapter/10.1007%2F978-3-030-88806-0_3
N2  - 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.
ER  -

CHALUPA, Marek a Jan STREJČEK. Backward Symbolic Execution with Loop Folding. Online. In Cezara Dragoi, Suvam Mukherjee, and Kedar S. Namjoshi. \textit{Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings}. Cham (Switzerland): Springer, 2021, s.~49-76. ISBN~978-3-030-88805-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-88806-0\_{}3.

Podrobný výpis o publikaci