Property-based Testing of Abstract Domains

Simmo Saan
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
Graduation Thesis type
Bachelor - Computer Science
Vesal Vojdani, Kalmer Apinis
Defence year