Property-based Testing of Abstract Domains

Name
Simmo Saan
Abstract
Static program analysis studies programs based on their source code, without executing them. One approach is to use abstract interpretation to determine a program's possible approximate states, which make up an abstract domain. If the used domain satisfies certain mathematical properties, then the analysis is sound according to the theory of abstract interpretation. When implementing a static analyzer it may happen that the domains contain bugs, which ruin the analysis and its soundness. Here a set of properties is compiled, which are used to find bugs from the Goblint analyzer via property-based testing. For this the necessary domain testing framework and element generators are implemented in Goblint. Finally the testing is conducted, issues identified and described. This shows that property-based testing can effectively be used to find bugs from abstract domains.
Graduation Thesis language
Estonian
Graduation Thesis type
Bachelor - Computer Science
Supervisor(s)
Vesal Vojdani, Kalmer Apinis
Defence year
2018
 
PDF