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.
Monotonic abstraction techniques : from parametric to software model checking / F. Alberti, S. Ghilardi, N. Sharygina. - In: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE. - ISSN 2075-2180. - 168:(2014), pp. 1-11. ((Intervento presentato al 1. convegno Workshop on Logics and model-checking for self- systems tenutosi a Bertinoro nel 2014 [10.4204/EPTCS.168.1].
Monotonic abstraction techniques : from parametric to software model checking
S. GhilardiSecondo
;
2014
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.File | Dimensione | Formato | |
---|---|---|---|
1411.3790v1.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
94.83 kB
Formato
Adobe PDF
|
94.83 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.