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

Student:

Jaehyung Jeff Cho

Partner:

Synopsys Canada ULC

Discipline:

Computer science

Sector:

Information and cultural industries

University:

University of Alberta