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.

Faculty Supervisor:

Dr. Béchir Ktari

Student:

François Lajeunesse-Robert

Partner:

RDDC Valcartier

Discipline:

Mathematics

Sector:

Information and communications technologies

University:

Université Laval