# 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. |

@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} }