Monotonic Abstraction Techniques: from Parametric to Software Model Checking

Francesco Alberti
(University of Lugano, Lugano, Switzerland )
Silvio Ghilardi
(Universià degli Studi di Milano, Milano, Italy)
Natasha Sharygina
(University of Lugano, Lugano, Switzerland)

Monotonic abstraction is a technique introduced in model checking parameterized distributed systems in order to cope with transitions containing global conditions within guards. The technique has been re-interpreted in a declarative setting in previous papers of ours and applied to the verification of fault tolerant systems under the so-called "stopping failures" model. The declarative reinterpretation consists in logical techniques (quantifier relativizations and, especially, quantifier instantiations) making sense in a broader context. In fact, we recently showed that such techniques can over-approximate array accelerations, so that they can be employed as a meaningful (and practically effective) component of CEGAR loops in software model checking too.

Invited Paper in Marcello Maria Bersani, Davide Bresolin, Luca Ferrucci and Manuel Mazzara: Proceedings First Workshop on Logics and Model-checking for Self-* Systems (MOD* 2014), Bertinoro, Italy, 12th September 2014, Electronic Proceedings in Theoretical Computer Science 168, pp. 1–11.
Published: 13th November 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: