Techniky pro ověřování ekvivalence původního a optimalizovaného kódu
| Název práce v češtině: | Techniky pro ověřování ekvivalence původního a optimalizovaného kódu |
|---|---|
| Název v anglickém jazyce: | Techniques for equivalence checking in the context of compiler optimizations |
| Akademický rok vypsání: | 2024/2025 |
| Typ práce: | diplomová 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: | |
| Konzultanti: | Mgr. Martin Blicha, Ph.D. |
| 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 corresponding to the code before and after performing the optimizations, should be involved. |
| 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/ |