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

- News
- Research
- Teaching
- Staff
- Martin Leucker
- Phillip Bende
- Martin Blankenburg
- Gerhard Buntrock
- David Caraveo
- Lukas Convent
- Normann Decker
- Sebastian Hungerecker
- Karam Kharraz
- Nikolas Knickrehm
- Christian Kreutzfeldt
- Felix Lange
- Grigory Markin
- Maria Ostanina
- André Pedro
- Torben Scheffel
- Malte Schmitz
- Nina Strugalla
- Annette Stümpel
- Daniel Thoma
- Dietmar Wolf
- Open Positions

- Contact