Paper Info
Title
Universal Invariant Checking Of Parametric Systems With Quantifier-Free Smt Reasoning
Abstract
The problem of invariant checking in parametric systems - which are required to operate correctly regardless of the number and connections of their components - is gaining increasing importance in various sectors, such as communication protocols and control software. Such systems are typically modeled using quantified formulae, describing the behaviour of an unbounded number of (identical) components, and their automatic verification often relies on the use of decidable fragments of first-order logic in order to effectively deal with the challenges of quantified reasoning.In this paper, we propose a fully automatic technique for invariant checking of parametric systems which does not rely on quantified reasoning. Parametric systems are modeled with array-based transition systems, and our method iteratively constructs a quantifier-free abstraction by analyzing, with SMT-based invariant checking algorithms for non-parametric systems, increasingly-larger finite instances of the parametric system. Depending on the verification result in the concrete instance, the abstraction is automatically refined by leveraging canditate lemmas from inductive invariants, or by discarding previously computed lemmas.We implemented the method using a quantifier-free SMT-based IC3 as underlying verification engine. Our experimental evaluation demonstrates that the approach is competitive with the state of the art, solving several benchmarks that are out of reach for other tools.
Year
DOI
Venue
2021
10.1007/978-3-030-79876-5_8
AUTOMATED DEDUCTION, CADE 28
Keywords
DocType
Volume
Parametric Systems, Array-based transitions systems, Abstraction-refinement, SMT
Conference
12699
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Alessandro Cimatti15064323.15
Alberto Griggio262436.37
Gianluca Redondi300.34