Target
Master thesis or Research project
Contact

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.

  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/