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. 1The 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