Thesis Details

Synthesizing Non-Termination Proofs from Templates

Master's Thesis Student: Martiček Štefan Academic Year: 2016/2017 Supervisor: Vojnar Tomáš, prof. Ing., Ph.D.
Czech title
Syntéza důkazů nekonečnosti běhu programů s využitím šablon
Language
English
Abstract

One of the properties that are most difficult to verify in the area of formal analysis is liveness. Proving non-termination of programs also belongs to the methods that verify this property. Our work describes the design and implementation of two algorithms checking non-termination. We inspire ourselves by already existing approaches, such as recurrence sets and over-approximation of loops with the use of invariants in the form of recurrence relations. The main challenge for us was an adaptation of these algorithms to the SSA (single static assignment) representation used in 2LS and the overall integration in our framework. We were able to unify the mentioned approaches into analysis of non-termination, which achieves the best results in comparison to the other tools that were compared at the SV-COMP 2017 competition.

Keywords

termination, non-termination, 2LS, bit-vectors, singleton recurrence set, periodical recurrence set

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology, Field of Study Intelligent Systems
Files
Status
defended, grade A
Date
20 June 2017
Reviewer
Fiedor Tomáš, Ing., Ph.D.
Committee
Zbořil František, doc. Ing., Ph.D. (DITS FIT BUT), předseda
Č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
Citation
MARTIČEK, Štefan. Synthesizing Non-Termination Proofs from Templates. Brno, 2017. Master's Thesis. Brno University of Technology, Faculty of Information Technology. 2017-06-20. Supervised by Vojnar Tomáš. Available from: https://www.fit.vut.cz/study/thesis/13436/
BibTeX 
@mastersthesis{FITMT13436,
    author = "\v{S}tefan Marti\v{c}ek",
    type = "Master's thesis",
    title = "Synthesizing Non-Termination Proofs from Templates",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2017,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/13436/"
}

Theses

Back to top