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.

Intern: 
Jaehyung Jeff Cho
Faculty Supervisor: 
Karim Ali
Province: 
Alberta
Partner University: 
Discipline: 
Program: