Název: Metody pro redukci velikosti interpolantů při použití částečného přiřazení
Překlad názvu: Methods for reduction of Craig's interpolant size using partial variable assignment
Autoři: Blicha, Martin ; Kofroň, Jan (vedoucí práce) ; Kučera, Petr (oponent)
Typ dokumentu: Diplomové práce
Rok: 2016
Jazyk: eng
Abstrakt: [eng] [cze]
Abstract. Since the introduction of interpolants to the field of symbolic model checking, interpolation-based methods have been successfully used in both hardware and software model checking. Recently, variable assignments have been introduced to the computation of interpolants. In the context of abstract reachability graphs, variable assignment can be used not only to prevent out-of-scope variables from appearing in interpolants, but also to reduce the size of the interpolant significantly. We further extend the framework for computing interpolants under variable assignment, prove the correctness of the system and show that it has potential to further decrease the size of the computed interpolants. At the end we analyze under which conditions the computed interpolants will still have the path interpolation property, a desired property in many interpolation-based techniques. 1 V čase, ktorý ubehol od prvého použitia interpolantov v oblasti symbolického overovania modelov (symbolic model checking), sa metódy založené na interpolantoch s úspechom uplatnili v oblasti overovania hardvéru aj softvéru. Prednedávnom sa v oblasti výpočtu interpolantov objavili čiastočné ohodnotenia premenných. V kontexte takzvaných "abstract reachability graphs" predstavujú čiatočné ohodnotenia spôsob ako sa zároveň elegantne vysporiadať s premennými mimo aktuálny kontext a zároveň dosiahnuť zmenšenie spočítaného interpolantu. V tejto práci sme ďalej rozvinuli systém pre počítanie interpolantov za prítomnosti čiastočných ohodnotení, dokázali sme jeho korektnosť a ukázali sme jeho potenciál pre ďalšie zmenšenie počítaných interpolantov. Nakoniec sme analyzovali za akých podmienok budú mať počítané interpolanty vlastnosť dôležitú pre mnoho techník založených na interpolácií - tzv. path interpolation property. Powered by TCPDF (www.tcpdf.org)
Klíčová slova: Craigova interpolace; symbolický model checking; Tseitinovo kódování; částečné přiřazení proměnných; Craig interpolation; partial variable assignment; symbolic model checking; Tseitin's encoding

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/82950

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


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Diplomové práce