Handling Heap Data Structures in Backward Symbolic Execution

Abstract:

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. In this paper, we present our achievements in this area. 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 conjunct combination. Second, we present a novel method for modelling 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 conjunct combination is the most efficient variant, exceeding the straightforward implementation of disjunct propagation in an order of magnitude.

BibTeX:

@inproceedings{husak_handling_2019,
    title = {{Handling Heap Data Structures in Backward Symbolic Execution}},
    author = {Husák, Robert and Kofroň , Jan and Zavoral, Filip},
    year = {2019},
    booktitle = {{Pre-proceedings for TAPAS 2019}},
    location = {Portugal},
    url = {https://staticanalysis.org/tapas2019/talks/tapas19-pre.pdf},
}

Proceedings paper