Název: Syntéza důkazů nekonečnosti běhu programů s využitím šablon
Překlad názvu: Synthesizing Non-Termination Proofs from Templates
Autoři: Martiček, Štefan ; Fiedor, Tomáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Typ dokumentu: Diplomové práce
Rok: 2017
Jazyk: eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [eng] [cze]
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. 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.
Klíčová slova: 2LS; bit-vectors; non-termination; periodical recurrence set; singleton recurrence set; termination; 2LS; bitové vektory; jednoprvková rekurentní množina; neukončitelnost; periodická rekurentní množina; ukončitelnost

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: http://hdl.handle.net/11012/69567

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-604455


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Diplomové práce