Techniky pro ověřování ekvivalence původního a optimalizovaného kódu
| Thesis title in Czech: | Techniky pro ověřování ekvivalence původního a optimalizovaného kódu |
|---|---|
| Thesis title in English: | Techniques for equivalence checking in the context of compiler optimizations |
| Academic year of topic announcement: | 2024/2025 |
| 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 |
| 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. |
| References |
| [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/ |