Název: STP řešič pro OpenSMT
Překlad názvu: STP solver for OpenSMT
Autoři: Luňák, Václav ; Kofroň, Jan (vedoucí práce) ; Kučera, Petr (oponent)
Typ dokumentu: Bakalářské práce
Rok: 2020
Jazyk: cze
Abstrakt: [cze] [eng]
Simple Temporal Problem je jedním z nejdůležitějších plánovacích problémů. V kontextu formální verifikace úzce souvisí s problémem SMT, kde na něj narazíme při řešení teorie dife- renční logiky. V této práci se věnujeme doplnění řešiče pro diferenční logiku do vyvíjejícího se SMT řešiče OpenSMT. Zkoumáme existující postupy pro řešení problému a porovnáváme je s ohledem na možnost jejich využití v kontextu OpenSMT. Detailně rozebíráme algoritmus založený na vyčerpávající propagaci teorie a na jeho bázi navrhujeme a vytváříme efektivní im- plementaci řešiče. Tuto implementaci následně testujeme a srovnáváme s ostatními současnými SMT řešiči a ukazujeme tak její srovnatelnou výkonnost. 1 The Simple Temporal Problem is one of the fundamental scheduling problems. In the context of formal verification, it is closely related to SMT, where we can encounter it while solving the theory of difference logic. In this work we create a solver for difference logic as a part of the OpenSMT solver. We look at existing approaches and evaluate their applicability to OpenSMT. Then we analyze an algorithm based on exhaustive theory propagation and use it to create an efficient implementation of the solver. This implementation is tested and compared to other current SMT solvers, proving its comparable efficiency. 1
Klíčová slova: diferenční logika; DPLL(T); OpenSMT; SMT; STP; difference logic; DPLL(T); OpenSMT; SMT; STP

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

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


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