MOVES Seminar, 1 Juni 2006
Inferring Network Invariants Automatically
Martin Leuker
TU München
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] \parallel \cdots \parallel P[n]$ can be carried
out.
In this talk, 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.
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] \parallel \cdots \parallel P[n]$ can be carried
out.
In this talk, 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.
