Monotonic Abstraction Techniques: from Parametric to Software Model Checking
This work addresses verification challenges in distributed and software systems, but it is incremental as it builds on prior reinterpretations and applications.
The paper tackles the problem of verifying parameterized distributed systems and software by adapting monotonic abstraction techniques, originally for global conditions, to broader contexts including array accelerations and CEGAR loops, showing practical effectiveness.
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.