Model Checking of Array-Based Systems: from Foundations to Implementation

We are interested in automatically proving safety properties of infinite state systems, by combining the classical algebraic approach of [4] with deductive techniques exploiting, off-the-shelf, SMT solvers. After briefly recalling the main contributions in [4] leading to the use of backward reachability analysis to prove safety properties and overviewing the long line of works stemming from that seminal paper (such as [9, 8, 5–7]), we present the notion of array based systems [10]. Such systems are declarative abstractions of several classes of parametrised systems and (sequential) programs manipulating arrays. In the framework of array based systems, key notions from [4] (such as configuration, configuration ordering, and monotonic transition) can be adapted and reused in a uniform and simple way. A by-product of this approach is to make readily available deductive techniques (like the synthesis and the use of invariants [11]) in the context of the algorithmic verification technique of backward reachability. This is so because the framework retains the modularity and the flexibility typical of logic-based approaches to modelchecking (in the same spirit of, e.g., [14]). The key feature of array-based systems is that a suitable format for initial/unsafe states and transition formulae can be designed: this format is sufficiently expressive to cover interesting classes of infinite state systems and, at the same time, generates proof obligations (during backward analysis) that can be discharged by instantiation and SMT solving techniques for quantifier-free formulae. To make the theoretical framework useful in practice, powerful heuristics are required to obtain adequate performances: these heuristics concern optimization of the computation of the pre-image [13], (static and dynamic) filtration of the instantiations that current SMT solvers cannot yet handle efficiently, as well as forward/backward simplification routines [12]. In the last part of the talk, we report our experimental experience with a prototype tool called mcmt [1], currently under development: we discuss its architecture (especially the interplay between the generation of proof obligations, the computation of pre-images, and the various heuristics) and its integration with the SMT solver Yices [3]; finally we compare mcmt with some state-of-the-art model checkers based on dedicated techniques like pfs [2]. This is joint work with Silvio Ranise (Universita di Verona).