Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories
Articolo
Data di Pubblicazione:
2012
Citazione:
Universal Guards, Relativization of Quantifiers, and Failure
Models in Model Checking Modulo Theories / F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, G.P. Rossi. - In: JOURNAL ON SATISFIABILITY, BOOLEAN MODELING AND COMPUTATION. - ISSN 1574-0617. - 8:(2012), pp. 29-61.
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 inter-
preted 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 transforma-
tion significantly extends the scope of applicability of the symbolic backward reachability
procedure. To provide empirical evidence of this claim, we discuss our findings in apply-
ing the proposed technique to a significant case-study in the verification of some classical
algorithms for reliable broadcast.
Tipologia IRIS:
01 - Articolo su periodico
Keywords:
model checking modulo theories; failure models; quantifiers instantiation;
reliable broadcast
Elenco autori:
F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, G.P. Rossi
Link alla scheda completa: