Affiliations: [a] Network Support System, Eolo SpA, via Gran San Bernardo, 12, 21052 Busto Arsizio, Italy. francesco.alberti@eolo.it | [b] Department of Mathematics, Università degli Studi di Milano, via Saldini, 50, 20133 Milano, Italy. silvio.ghilardi@unimi.it | [c] Faculty of Informatics, Università della Svizzera Italiana, via G. Buffi, 13, CH-6900 Lugano, Switzerland. natasha.sharygina@usi.ch
Correspondence:
[C]
Address for correspondence: Network Support System, Eolo SpA, via Gran San Bernardo, 12, 21052 Busto Arsizio, Italy
Note: [*] This paper combines and extends materials previously published in [1, 2].
Note: [†] This work was conducted while the first author was at the Universitá della Svizzera Italiana.
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.
