# Inferring Network Invariants Automatically

 Title Inferring Network Invariants Automatically Publication Type Conference Paper Year of Publication 2006 Authors Grinchtein, O, Leucker, M, Piterman, N Conference Name Proceedings of the 3rd International Joint Conference on Automated Reasoning {(IJCAR'06)} Series Lecture Notes in Artificial Itelligence Volume 4130 Abstract Verification by network invariants is a heuristic to solve uniform verification of parameterized systems. Given a system P, a network invariant for P is a system that abstracts the composition of every number of copies of P running in parallel. If there is such a network invariant, by reasoning about it, uniform verification with respect to the family P[1] || ... || P[n] can be carried out. In this paper, we propose a procedure searching systematically for a network invariant satisfying a given safety property. The search is optimized using a combination of Angluin's and Biermann's learning/inference algorithms for improving successively possible invariants. We also show how to reduce the learning problem to SAT, allowing efficient SAT solvers to be used, which turns out to yield a very competitive learning algorithm. The overall search procedure finds a minimal such invariant, if it exists.
Bibtex:
@inproceedings {GrinchteinLP06,
title = {Inferring Network Invariants Automatically},
booktitle = {Proceedings of the 3rd International Joint Conference on Automated Reasoning {(IJCAR{\textquoteright}06)}},
series = {Lecture Notes in Artificial Itelligence},
volume = {4130},
year = {2006},
abstract = {Verification by network invariants is a heuristic to solve uniform verification of parameterized systems. Given a system P, a network invariant for P is a system that abstracts the composition of every number of copies of P running in parallel. If there is such a network invariant, by reasoning about it, uniform verification with respect to the family P[1] || ... || P[n] can be carried out. In this paper, we propose a procedure searching systematically for a network invariant satisfying a given safety property. The search is optimized using a combination of Angluin{\textquoteright}s and Biermann{\textquoteright}s learning/inference algorithms for improving successively possible invariants. We also show how to reduce the learning problem to SAT, allowing efficient SAT solvers to be used, which turns out to yield a very competitive learning algorithm. The overall search procedure finds a minimal such invariant, if it exists.},
author = {Olga Grinchtein and Martin Leucker and Nir Piterman}
}
PDF:
Postscript: