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. Ghilardi
Secondo
;
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.
Infinite-state systems; Software model-checking; Arrays; Quantifiers; Satisfiability; Modulo Theories
Settore INF/01 - Informatica
2017
Article (author)
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/464858
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 5
social impact