Flow-sensitive and flow-insensitive program analyses occupy opposite ends of a spectrum. Between these extremes lie mixed flow-sensitive approaches in which some aspects of program behavior are analyzed flow-insensitively and others flow-sensitively. Mixed flow-sensitivity arises, for example, in the thread-modular analysis of multi-threaded code or when global-store widening is used to improve scalability.

The tutorial covers both the foundations of mixed flow-sensitive analysis and practical aspects. We first introduce and motivate mixed flow-sensitivity along some examples before presenting a convenient formalism for specifying such analyses independent of the chosen means of fixpoint computation. We then present the Goblint static analysis framework, which can be used to rapidly prototype and implement novel mixed flow-sensitive analyses. Participants will then get their feet wet as we gently guide them through the implementation of a simple mixed flow-sensitive analysis in Goblint.

For the hands-on session, we recommend having the Goblint static analyzer installed. Detailed installation instructions will appear at http://goblint.in.tum.de/tutorial closer to the date of the tutorial.