Monotonic abstraction techniques: From parametric to software model checking

Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationElectronic Proceedings in Theoretical Computer Science, EPTCS
PublisherOpen Publishing Association
Pages1-11
Number of pages11
Volume168
DOIs
Publication statusPublished - Nov 13 2014
Event1st Workshop on Logics and Model-checking for Self-* Systems, MOD* 2014 - Bertinoro, Italy
Duration: Sep 12 2014 → …

Other

Other1st Workshop on Logics and Model-checking for Self-* Systems, MOD* 2014
CountryItaly
CityBertinoro
Period9/12/14 → …

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Monotonic abstraction techniques: From parametric to software model checking'. Together they form a unique fingerprint.

  • Cite this

    Alberti, F., Ghilardi, S., & Sharygina, N. (2014). Monotonic abstraction techniques: From parametric to software model checking. In Electronic Proceedings in Theoretical Computer Science, EPTCS (Vol. 168, pp. 1-11). Open Publishing Association. https://doi.org/10.4204/EPTCS.168.1