Thesis Details
Improving Precision of Program Analysis in the 2LS Framework
The goal of this work is to propose a way to improve precision of program analysis in the 2LS framework, based on its existing concepts, mainly template-based synthesis of invariants. 2LS is a static analysis framework for analysing C programs which relies on the use of an SMT solver and of abstract interpretation for automatic invariant inference. In a case when 2LS can not decide whether a program is correct, the proposed solution analyses the invariants computed in various abstract domains and identifies parts of the invariants that potentially cause undecidability of the verification. Using the obtained information, the designed method is able to identify variables of the original program that possibly determine whether the verification is successful. The output of our solution can be used as a feedback to indicate variables with problematic values that should be constrained. Also, it can be utilized by the 2LS developers for debugging purposes during development of new analyses. The solution has been implemented in the 2LS framework. Testing our solution on various benchmarks from the International Competition on Software Verification (SV-COMP) shows that it can identify variables that cause undecidability of the verification in more than half of the programs where the verification currently fails.
formal verification, program analysis, static analysis, 2LS, abstract interpretation, invariant, SSA form, abstract domain, template-based analysis
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Honzík Jan M., prof. Ing., CSc. (DIFS FIT BUT), člen
Kořenek Jan, doc. Ing., Ph.D. (DCSY FIT BUT), člen
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT), člen
@bachelorsthesis{FITBT21638,
author = "Martin Smutn\'{y}",
type = "Bachelor's thesis",
title = "Improving Precision of Program Analysis in the 2LS Framework",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2019,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/21638/"
}