We present our framework for the verification of parameterized infinite-state systems. The framework has been successfully applied in the verification of heterogeneous systems, ranging from distributed fault-tolerant protocols to programs handling unbounded data-structures. In such application domains, being able to infer quantified invariants is a mandatory requirement for successful results. Our framework differentiates itself from the state-of-the-art solutions targeting the generation of quantified safe inductive invariants: instead of monolitically exploiting a single static analysis technique, it is based on the effective integration of several analysis strategies. The paper targets the description of the engineering strategies adopted for a successful implementation of such an integrated framework, and presents the extensive experimental evaluation demonstrating its effectiveness.
A Framework for the Verification of Parameterized Infinite-state Systems / F. Alberti, S. Ghilardi, N. Sharygina. - In: FUNDAMENTA INFORMATICAE. - ISSN 0169-2968. - 150:1(2017), pp. 1-24. [10.3233/FI-2017-1458]
A Framework for the Verification of Parameterized Infinite-state Systems
S. GhilardiSecondo
;
2017
Abstract
We present our framework for the verification of parameterized infinite-state systems. The framework has been successfully applied in the verification of heterogeneous systems, ranging from distributed fault-tolerant protocols to programs handling unbounded data-structures. In such application domains, being able to infer quantified invariants is a mandatory requirement for successful results. Our framework differentiates itself from the state-of-the-art solutions targeting the generation of quantified safe inductive invariants: instead of monolitically exploiting a single static analysis technique, it is based on the effective integration of several analysis strategies. The paper targets the description of the engineering strategies adopted for a successful implementation of such an integrated framework, and presents the extensive experimental evaluation demonstrating its effectiveness.File | Dimensione | Formato | |
---|---|---|---|
fi-150(1)02.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
637.25 kB
Formato
Adobe PDF
|
637.25 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.