Thesis Details
Template-Based Synthesis of Heap Abstractions
The goal of this work is to propose a shape analysis suitable for the context of the 2LS analyser. 2LS is a program analysis framework for C programs which is based on automatic invariant inference using an SMT solver. The proposed solution includes a way how the shape of a program heap can be described using logical formulae over bit-vectors and how a first-order SMT solver can be used to infer loop invariants and function summaries for each function of the analysed program. Our approach is based on pointer access paths that describe the shape of the heap by expressing the reachability of heap objects from pointer-typed program variables. The information obtained from the analysis can be used to prove various properties of programs manipulating dynamic data structures, mainly linked lists. The solution has been implemented in the 2LS framework and it brought a significant improvement in terms of the capabilities of 2LS in analysing heap-manipulating programs. This is demonstrated on benchmarks taken from the well-known International Competition on Software Verification (SV-COMP) as well as other benchmarks.
formal verification, program analysis, 2LS, template-based analysis, shape analysis, linked lists, pointer access paths, abstract interpretation, SSA form, invariant inference, function summaries, dynamic data structures
Čadík Martin, doc. Ing., Ph.D. (DCGM FIT BUT), člen
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT), člen
Janoušek Jan, doc. Ing., Ph.D. (FIT CTU), člen
Orság Filip, Ing., Ph.D. (DITS FIT BUT), člen
Zachariášová Marcela, Ing., Ph.D. (DCSY FIT BUT), člen
@mastersthesis{FITMT19901,
author = "Viktor Mal\'{i}k",
type = "Master's thesis",
title = "Template-Based Synthesis of Heap Abstractions",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2017,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/19901/"
}