Kalmer Apinis. Frameworks for analyzing multi-threaded C. PhD thesis, Institut für Informatik, Technische Universität München June 2014.

We show how side-effecting constraint systems provide a unified framework for realizing efficient inter-procedural analyses of programs, where the amount of context-sensitivity can be adjusted and where the context-sensitive analyses of local properties can be combined with flow-insensitive analyses of global properties. To use the widening and narrowing approach on (side-effecting) constraint systems, we present a novel operator together with adapted versions of solving algorithms. Finally, we report on the various implementation challenges that arose in the Goblint tool.

Download: PDF Reference: Bibtex