Handling Heap Data Structures in Backward Symbolic Execution

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F20%3A10397704" target="_blank" >RIV/00216208:11320/20:10397704 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-54997-8_33" target="_blank" >https://doi.org/10.1007/978-3-030-54997-8_33</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-54997-8_33" target="_blank" >10.1007/978-3-030-54997-8_33</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Handling Heap Data Structures in Backward Symbolic Execution

Popis výsledku v původním jazyce

Backward symbolic execution (BSE), also known as weakest precondition computation, is a useful technique to determine validity of assertions in program code by transforming its semantics into boolean conditions for an SMT solver. Regrettably, the literature does not cover various challenges which arise during its implementation, especially when we want to reason about heap objects using the theory of arrays and to use the SMT solver efficiently. Our contribution is threefold. First, we summarize the two most popular state-of-the-art approaches used for BSE, denoting them as disjunct propagation and conjunction combination. Second, we present a novel method how to model heap operations in BSE using the theory of arrays, optimized for incremental checking during the analysis and handling the input heap. Third, we compare both approaches with our heap handling implementation on a set of program examples, presenting their strengths and weaknesses. The evaluation shows that the conjunction combination approach with incremental solving is the most efficient variant, exceeding straightforward implementation of disjunct propagation in an order of magnitude.

Název v anglickém jazyce

Handling Heap Data Structures in Backward Symbolic Execution

Popis výsledku anglicky

Backward symbolic execution (BSE), also known as weakest precondition computation, is a useful technique to determine validity of assertions in program code by transforming its semantics into boolean conditions for an SMT solver. Regrettably, the literature does not cover various challenges which arise during its implementation, especially when we want to reason about heap objects using the theory of arrays and to use the SMT solver efficiently. Our contribution is threefold. First, we summarize the two most popular state-of-the-art approaches used for BSE, denoting them as disjunct propagation and conjunction combination. Second, we present a novel method how to model heap operations in BSE using the theory of arrays, optimized for incremental checking during the analysis and handling the input heap. Third, we compare both approaches with our heap handling implementation on a set of program examples, presenting their strengths and weaknesses. The evaluation shows that the conjunction combination approach with incremental solving is the most efficient variant, exceeding straightforward implementation of disjunct propagation in an order of magnitude.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA17-12465S" target="_blank" >GA17-12465S: Verifikace a hledání chyb v pokročilém softwaru</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2020

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

Formal Methods. FM 2019 International Workshops

ISBN

978-3-030-54997-8

ISSN

—

e-ISSN

—

Počet stran výsledku

20

Strana od-do

537-556

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Porto

Datum konání akce

7. 10. 2019

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

WRD - Celosvětová akce

Kód UT WoS článku

—