%0 Journal Article %1 kedar2007symmetry %A Namjoshi, Kedar %D 2007 %J Verification, Model Checking, and Abstract Interpretation %K assertional completeness cutoff invariants parameterized quantified_invariants verification %P 299--313 %T Symmetry and Completeness in the Analysis of Parameterized Systems %U http://dx.doi.org/10.1007/978-3-540-69738-1_22 %X It is shown that the cutoff method—which summarizes a parameterized system by a finite set of its instances—is complete for proving safety properties. This implies completeness of other, less stringent, proof methods for parameterized verification. It is shown that the cutoffmethod is equivalent to determining a (parameterized) inductive invariant. The second part of the paper describes a new algorithmto construct universally quantified, parameterized inductive invariants. This algorithm is shown to compute the strongest invariant of a given shape, and is complete under certain conditions. A key observation is a previously unnoticed connectionbetween inductiveness, small model theorems, and compositional analysis.

@article{kedar2007symmetry, abstract = {It is shown that the cutoff method—which summarizes a parameterized system by a finite set of its instances—is complete for proving safety properties. This implies completeness of other, less stringent, proof methods for parameterized verification. It is shown that the cutoffmethod is equivalent to determining a (parameterized) inductive invariant. The second part of the paper describes a new algorithmto construct universally quantified, parameterized inductive invariants. This algorithm is shown to compute the strongest invariant of a given shape, and is complete under certain conditions. A key observation is a previously unnoticed connectionbetween inductiveness, small model theorems, and compositional analysis.}, added-at = {2010-05-01T19:35:07.000+0200}, author = {Namjoshi, Kedar}, biburl = {https://www.bibsonomy.org/bibtex/259cdb6a353774faf8da62e5995cb60a0/giuliano.losa}, description = {Symmetry and Completeness in the Analysis of Parameterized Systems}, interhash = {e098c623ea27aab708250a481035008b}, intrahash = {59cdb6a353774faf8da62e5995cb60a0}, journal = {Verification, Model Checking, and Abstract Interpretation}, keywords = {assertional completeness cutoff invariants parameterized quantified_invariants verification}, pages = {299--313}, timestamp = {2010-05-01T19:35:07.000+0200}, title = {Symmetry and Completeness in the Analysis of Parameterized Systems}, url = {http://dx.doi.org/10.1007/978-3-540-69738-1_22}, year = 2007 }