Inferring Network Invariants Automatically

11 years 4 days ago
Inferring Network Invariants Automatically
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 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 that searches systematically for a network invariant satisfying a given safety property. The search is based on algorithms for learning finite automata due to Angluin and Biermann. We optimize the search by combining both algorithms for improving successive 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.
Olga Grinchtein, Martin Leucker, Nir Piterman
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where CADE
Authors Olga Grinchtein, Martin Leucker, Nir Piterman
Comments (0)