Handling Heap Data Structures in Backward Symbolic Execution
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Handling Heap Data Structures in Backward Symbolic Execution
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA17-12465S" target="_blank" >GA17-12465S: Verification and Bug Hunting for Advanced Software</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2020
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Formal Methods. FM 2019 International Workshops
ISBN
978-3-030-54997-8
ISSN
—
e-ISSN
—
Number of pages
20
Pages from-to
537-556
Publisher name
Springer
Place of publication
Cham
Event location
Porto
Event date
Oct 7, 2019
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—