Techniky pro ověřování ekvivalence překladačových optimalizací
| Název práce v češtině: | Techniky pro ověřování ekvivalence překladačových optimalizací |
|---|---|
| Název v anglickém jazyce: | Techniques for equivalence checking in the context of compiler optimizations |
| Akademický rok vypsání: | 2025/2026 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | doc. RNDr. Jan Kofroň, Ph.D. |
| Řešitel: |
| Zásady pro vypracování |
| Verification of correctness of compiler optimizations can be done by checking the equivalence of the optimized and unoptimized version (they have the same input-output relation, i.e., they provide the same outputs for the same inputs) of the processed code.
The goal of this thesis is, for various compiler optimizations, especially those considering code with loops, to survey available techniques for verification of their correctness and their shortcomings [1] and improve on them. Among considered approaches, equivalence checking, involving SMT and CHC queries [2] corresponding to the code before and after performing the optimizations, is a possible way. As the preferred realization platform, LLVM [3] should be considered. The proposed solution should be implemented; a suitable subset of the input language/intermediate language features is to be chosen to support. |
| Seznam odborné literatury |
| [1] Lopes, N.P., Monteiro, J. Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. Int J Softw Tools Technol Transfer 18, 359–374 (2016). https://doi.org/10.1007/s10009-015-0366-1
[2] Horn clauses: https://en.wikipedia.org/wiki/Horn_clause [3] LLVM project: https://llvm.org/ |