Rozhodovací procedura pro lineární celočíselnou aritmetiku v moderním SMT řešiči
| Thesis title in Czech: | Rozhodovací procedura pro lineární celočíselnou aritmetiku v moderním SMT řešiči |
|---|---|
| Thesis title in English: | Decision procedure for Linear Integer Arithmetic for modern SMT solver |
| Academic year of topic announcement: | 2023/2024 |
| Thesis type: | diploma thesis |
| Thesis language: | |
| Department: | Department of Distributed and Dependable Systems (32-KDSS) |
| Supervisor: | doc. RNDr. Jan Kofroň, Ph.D. |
| Author: | |
| Advisors: | Mgr. Martin Blicha, Ph.D. |
| Guidelines |
| SMT solvers are software tools for deciding about satisfiability of formulas in first-order logics. They are powerful reasoning engines successfully used in applications such as verification of software.
Linear Integer Arithmetic is a popular language for modelling verification problems, providing a good trade-off between precision and solvability. The goal of the thesis is to implement a decision procedure for Linear Integer Arithmetic according to latest research results in the OpenSMT solver [1], and evaluate its performance, preferably using benchmarks from [2]. |
| References |
| [1] OpenSMT: https://github.com/usi-verification-and-security/opensmt/
[2] SMT-LIB: http://smtlib.cs.uiowa.edu [3] SMT-COMP: https://smt-comp.github.io/2019/ |