Thesis Details
Generic Template-Based Synthesis of Program Abstractions
The goal of this work is to design and to implement a generic strategy solver to the 2LS tool.2LS is an analyser for a static verification of programs written in C language. A verifiedprogram is analysed by an SMT solver using abstract interpretation. Convertion from anabstract state of the program into a logical formula, that an SMT solver can work with, isdone by a component called strategy solver. In the current implementation, there is onestrategy solver for each abstract domain. Our approach introduces a single generic strategysolver, which makes creating new domains easier. Also, this approach enables migration ofthe existing domains and hence the codebase can be reduced.
formal verification, 2LS, static analysis, SSA form, abstract domain, strategy solver, SMTsolving, abstract interpretation
Beran Vítězslav, doc. Ing., Ph.D. (DCGM FIT BUT), člen
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Janoušek Jan, doc. Ing., Ph.D. (FIT CTU), člen
Peringer Petr, Dr. Ing. (DITS FIT BUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT), člen
@mastersthesis{FITMT21674,
author = "Matej Maru\v{s}\'{a}k",
type = "Master's thesis",
title = "Generic Template-Based Synthesis of Program Abstractions",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2019,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/21674/"
}