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.
|Titolo:||A Framework for the Verification of Parameterized Infinite-state Systems|
GHILARDI, SILVIO (Secondo)
|Parole Chiave:||Infinite-state systems; Software model-checking; Arrays; Quantifiers; Satisfiability; Modulo Theories|
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
|Data di pubblicazione:||2017|
|Digital Object Identifier (DOI):||10.3233/FI-2017-1458|
|Appare nelle tipologie:||01 - Articolo su periodico|