Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories
Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi · Journal on Satisfiability Boolean Modeling and Computation · 2012
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 (un