Relational Thread-Modular Static Value Analysis by Abstract Interpretation?

Abstract. We study thread-modular static analysis by abstract inter-pretation to infer the values of variables in concurrent programs. We show how to go beyond the state of the art and increase an analysis pre-cision by adding the ability to infer some relational and history-sensitive properties of thread interferences. The fundamental basis of this work is the formalization by abstract interpretation of a rely-guarantee concrete semantics which is thread-modular, constructive, and complete for safety properties. We then show that previous analyses based on non-relational interferences can be retrieved as coarse computable abstractions of this semantics; additionally, we present novel abstraction examples exploit-ing our ability to reason more precisely about interferences, including domains to infer relational lock invariants and the monotonicity of coun-ters. Our method and domains have been implemented in the AstréeA static analyzer that checks for run-time errors in embedded concurrent C programs, where they enabled a significant reduction of the number of false alarms