Abstract domains for property checking driven analysis of temporal properties

Abstract

interpretation-based static analysis infers properties from the source code of a program. When the goal is to check a temporal specification on the program, we need the analysis to be as precise as possible to avoid false negatives. In previous work [9], we suggested a method called "property checking driven analysis" to automatically use the specification to check during the analysis hi order to refine it. However, this approach requires to abstract domains of lower closure operators, something which was not developed. In this paper, we describe some abstractions on lower closure operators developed for a small analyzer of temporal properties. We examine the need for weak relational abstractions, and show that using our new approach can give more precise results than using a traditional abstract interpretation-based analysis with expensive abstract domains. © Springer-Verlag 2004.