Original title: STP řešič pro OpenSMT
Translated title: STP solver for OpenSMT
Authors: Luňák, Václav ; Kofroň, Jan (advisor) ; Kučera, Petr (referee)
Document type: Bachelor's theses
Year: 2020
Language: cze
Abstract: [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
Keywords: difference logic; DPLL(T); OpenSMT; SMT; STP; diferenční logika; DPLL(T); OpenSMT; SMT; STP

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/121027

Permalink: http://www.nusl.cz/ntk/nusl-434970


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Bachelor's theses