Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis

The safety of infinite state systems can be checked by a backwardreachability procedure. For certain classes of systems, it is possible to provethe termination of the procedure and hence conclude the decidability of thesafety problem. Although backward reachability is property-directed, it canunnecessarily explore (large) portions of the state space of a system which arenot required to verify the safety property under consideration. To avoid this,invariants can be used to dramatically prune the search space. Indeed, theproblem is to guess such appropriate invariants. In this paper, we present afully declarative and symbolic approach to the mechanization of backwardreachability of infinite state systems manipulating arrays by SatisfiabilityModulo Theories solving. Theories are used to specify the topology and the datamanipulated by the system. We identify sufficient conditions on the theories toensure the termination of backward reachability and we show the completeness ofa method for invariant synthesis (obtained as the dual of backwardreachability), again, under suitable hypotheses on the theories. We alsopresent a pragmatic approach to interleave invariant synthesis and backwardreachability so that a fix-point for the set of backward reachable states ismore easily obtained. Finally, we discuss heuristics that allow us to derive animplementation of the techniques in the model checker MCMT, showing remarkablespeed-ups on a significant set of safety problems extracted from a variety ofsources.Comment: Accepted for publication in Logical Methods in Computer Scienc