Enhancing Logico-Numerical Abstract Interpretation Methods

We are interested in the verification of safety properties of synchronous data-flow programs with Boolean and numerical variables, e.g., Lustre programs. Our methods rely on inferring invariants with the help of an abstract interpretation-based reachability analysis. In order to ensure the termination of such an analysis, abstract interpretation uses an extrapolation operator (widening) which often results in an important loss of precision. Several methods have been proposed to overcome this problem: Abstract acceleration computes a precise extrapolation for a restricted class of transformations in loops, and hence, it reduces the need for widening. More recently, strategy iteration methods have been considered, which guarantee to compute best inductive invariants w.r.t. template domains. All these techniques, however, require the enumeration of the Boolean state-space, which leads to a state-space explosion even for medium-sized Lustre programs. In this talk we focus on abstract acceleration and we extend it from numerical to logico-numerical programs without resorting to the enumeration of the Boolean state-space. We define a logico-numerical abstract acceleration method based on a partial decoupling of Boolean and numerical transitions and we explain how a well-chosen partitioning technique makes it effective. Experimental results show that these methods provide not only an advantage in terms of precision but also a gain in performance.