Michael Schwarz

National University of Singapore, Singapore

Michael Schwarz

Michael Schwarz

National University of Singapore, Singapore

Lecture 6

Mixed Flow-Sensitive Abstract Interpretation with Goblint

Abstract

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

In this talk, we introduce mixed flow-sensitive analysis, sketch a convenient formalism, and present the Goblint static analysis framework, which can be used to rapidly prototype and implement novel mixed flow-sensitive analyses.