An Algebra-Based Approach to Program Verification

We want to study the feasibility of using an algebra-based approach to performing program analysis. In particular, we are interested in the code comparison problem: tackling this problem enables us, among other things, to identify differences between two versions of a code or to check whether an optimized code is equivalent to its non-optimized version. We aim to reduce the comparison of programs to a simple algebraic manipulation similar to those that are constantly performed in classical algebra.