Název: Rozbalování smyček programů v nástroji 2LS
Překlad názvu: Program Loop Unwinding in the 2LS Framework
Autoři: Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2022
Jazyk: eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [eng] [cze]
Cílem této práce je navrhnout vylepšený mechanismus rozbalování smyček pro analyzátor 2LS. 2LS je nástroj pro statickou analýzu C programů založený na usuzování o programech pomocí SMT solveru. Kombinuje několik běžných verifikačních technik do algoritmu zvaného k I k I. Jednou z klíčových součástí tohoto algoritmu je rozbalování smyček programu. Současné řešení bohužel neumožňuje správně rozbalovat smyčky obsahující operace s dynamicky alokovanou pamětí. Námi navrhované řešení je založeno na rozbalování smyček v GOTO programu namísto SSA formy, díky čemuž je možné správně pracovat s dynamickými objekty a operacemi s nimi. Navržené řešení bylo implementováno v nástroji 2LS a naše experimenty na sadě testů z mezinárodní soutěže ve verifikaci software (SV-COMP) ukazují, že zvyšuje korektnost analýzy programů pracujících s dynamickými objekty. 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 k I k I. 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.
Klíčová slova: 2LS Framework; bounded model checking; dynamic memory; formal verification; GOTO programs; k -induction; loop unwinding; program analysis; SSA form; static analysis; analýza programů; bounded model checking; dynamická paměť; formální verifikace; GOTO programy; k -indukce; nástroj 2LS; rozbalování smyček; SSA forma; statická analýza

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/207322

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


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 > Bakalářské práce