SMT model checking for array-based systems: foundations, invariant synthesis, benchmarks, case studies
We show how to exploit SMT solvers in declarative formulations of classical backward reachability algorithms. We motivate the notion of an array-based system and introduce some decision problems for quantified formulae arising from infinite state model checking applications. We also show how this framework is implemented in the model checker MCMT (based on the SMT solver Yices). Finally we discuss some common benchmarks in the area of distributed algorithms and report also recent experiments concerning timed and fault tolerant systems. We shall discuss the efficiency of strategies for invariant synthesis and for partially interactive verification in our experiments.