Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories

Abstract

Model Checking Modulo Theories is a recent approach for the automated verification of safety properties of a class of infinite state systems manipulating arrays, called array-based systems. The idea is to repeatedly compute pre-images of a set of (unsafe) states by using certain classes of first-order formulae representing sets of states and transitions, and then reduce fix-point checks to Satisfiability Modulo Theories problems. Unfortunately, if the guards contain universally quantified index variables, the backward procedure cannot be fully automated. In this paper, we overcome the problem by describing a syntactic transformation on array-based systems, which can be seen as an instance of the well-known operation of relativization of quantifiers in first-order logic. Interestingly, when specifying and verifying distributed systems, the proposed syntactic transformation can be interpreted as the adoption of the crash-failure model, which is well-known in the literature of fault-tolerant systems. By eliminating universal quantifiers from guards, the transformation significantly extends the scope of applicability of the symbolic backward reachability procedure. To provide empirical evidence of this claim, we discuss our findings in applying the proposed technique to a significant case-study in the verification of some classical algorithms for reliable broadcast.