Thesis Details

Program Loop Unwinding in the 2LS Framework

Bachelor's Thesis Student: Nečas František Academic Year: 2021/2022 Supervisor: Malík Viktor, Ing.
Czech title
Rozbalování smyček programů v nástroji 2LS
Language
English
Abstract

The goal of this work is to propose an improved unwinding mechanism for the 2LS formal verification tool. 2LS is a static analysis framework for C programs based on reasoning about programs using an SMT solver. It combines multiple common verification techniques into an algorithm called kIkI. One of the crucial parts of the algorithm is loop unwinding. Unfortunately, the existing solution does not correctly support unwinding of loops containing operations with dynamically allocated memory. Our proposed solution is based on unwinding loops in a GOTO program rather than the SSA form, making it possible to correctly handle dynamic objects and operations over them. The proposed solution has been implemented in the 2LS framework and our experiments on a set of benchmarks from the International Competition on Software Verification (SV-COMP) show that it improves soundness of analysis of programs working with dynamic objects.

Keywords

program analysis, formal verification, static analysis, 2LS Framework, loop unwinding, k-induction, bounded model checking, SSA form, GOTO programs, dynamic memory

Department
Degree Programme
Files
Status
defended, grade A
Date
13 June 2022
Reviewer
Committee
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Martínek Tomáš, Ing., Ph.D. (DCSY FIT BUT), člen
Peringer Petr, Dr. Ing. (DITS FIT BUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT), člen
Citation
NEČAS, František. Program Loop Unwinding in the 2LS Framework. Brno, 2022. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2022-06-13. Supervised by Malík Viktor. Available from: https://www.fit.vut.cz/study/thesis/24719/
BibTeX
@bachelorsthesis{FITBT24719,
    author = "Franti\v{s}ek Ne\v{c}as",
    type = "Bachelor's thesis",
    title = "Program Loop Unwinding in the 2LS Framework",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2022,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/24719/"
}
Back to top