Detail práce

Synthesizing Non-Termination Proofs from Templates

Diplomová práce Student: Martiček Štefan Akademický rok: 2016/2017 Vedoucí: Vojnar Tomáš, prof. Ing., Ph.D.
Název česky
Syntéza důkazů nekonečnosti běhu programů s využitím šablon
Jazyk práce
anglický
Abstrakt

Jednou z nejsložitěji verifikovaných vlastností programů v oblasti formální analýzy je živost. K jedné z metod ověřujících tuto vlastnost patří i dokazování neukončitelnosti programů. Naše práce popisuje návrh a implementaci dvou algoritmů ověřujících neukončitelnost. Inspirujeme se již existujícími přístupy, jako jsou rekurentní množiny a nadaproximace cyklů s využitím invariantů ve tvaru rekurentních relací. Hlavní výzvu pro nás představovalo přizpůsobení těchto algoritmů SSA (single static assignment) reprezentaci použité v 2LS a jejich celková integrace v našem frameworku. Vzpomínané přístupy se nám podařilo spojit do analýzy neukončitelnosti, která dosahuje nejlepší výsledky v porovnání s existujícími nástroji, které byly srovnané na soutěži SV-COMP 2017.

Klíčová slova

ukončitelnost, neukončitelnost, 2LS, bitové vektory, jednoprvková rekurentní množina, periodická rekurentní množina

Ústav
Ústav inteligentních systémů FIT VUT v Brně
Studijní program
Informační technologie, obor Inteligentní systémy
Soubory
Stav
obhájeno, hodnocení A
Obhajoba
20. června 2017
Oponent
Fiedor Tomáš, Ing., Ph.D.
Průběh obhajoby

Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm A - výborně.

Otázky u obhajoby
  1. Výsledná strategie využívá metodu SRS a po určitém počtu kroků (v kódu se jedná o magickou konstantu 51) se jednou použije metoda PRS a pak zas pokračuje přes SRS. Na základě čeho jste zvolil tento prah (51 kroků)?
  2. Stručně diskutujte potenciální rozšíření Vašeho přístupu na programy manipulující s dynamickými datovými strukturami.
Komise
Zbořil František, doc. Ing., Ph.D. (UITS FIT VUT), předseda
Čadík Martin, doc. Ing., Ph.D. (UPGM FIT VUT), člen
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT), člen
Janoušek Jan, doc. Ing., Ph.D. (FIT ČVUT), člen
Orság Filip, Ing., Ph.D. (UITS FIT VUT), člen
Zachariášová Marcela, Ing., Ph.D. (UPSY FIT VUT), člen
Citace
MARTIČEK, Štefan. Synthesizing Non-Termination Proofs from Templates. Brno, 2017. Diplomová práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2017-06-20. Vedoucí práce Vojnar Tomáš. Dostupné z: https://www.fit.vut.cz/study/thesis/13436/
BibTeX 
@mastersthesis{FITMT13436,
    author = "\v{S}tefan Marti\v{c}ek",
    type = "Diplomov\'{a} pr\'{a}ce",
    title = "Synthesizing Non-Termination Proofs from Templates",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2017,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/13436/"
}

Závěrečné práce

Nahoru