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. Moreover, the proposed approach could be used in other programming contexts such as program analysis; two examples are program synthesis and model checking.