Automatic Verification of Comparators and Hash Functions

The implementation of data structures usually requires checking for certain mathematical properties such as equality. Those properties are usually implemented in methods that reason about the objects stored in these data structures. However, the implementation of such methods is fairly complex, and may exhibit software bugs that may not necessarily lead to program crashes. Therefore, it is often hard to reproduce such bugs. This project aims at developing an automatic method that verifies the correctness of the implementation of such methods, without the need to reproduce the bugs that may result from incorrect implementations. Our focus will be comparators and hash functions as prime examples of such methods that check for mathematical properties.

Faculty Supervisor:

Karim Ali


Jaehyung Jeff Cho


Synopsys Canada ULC


Computer science


Information and cultural industries


University of Alberta



Current openings

Find the perfect opportunity to put your academic skills and knowledge into practice!

Find Projects