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.

Intern: 
François Lajeunesse-Robert
Faculty Supervisor: 
Dr. Béchir Ktari
Province: 
Quebec
University: 
Partner: 
Discipline: 
Program: