Efficient verification of network reachability properties

Network management will benefit from automated tools based upon formal methods. Several such tools have been published in the literature. We present a new formal method for a new tool, Atomic Predicates (AP) Verifier, which is much more time and space efficient than existing tools. Given a set of predicates representing packet filters, AP Verifier computes a set of atomic predicates, which is minimum and unique. We evaluated the performance of AP Verifier using forwarding tables and ACLs from three large real networks. The atomic predicate sets of these networks were computed very quickly and their sizes are surprisingly small. The use of atomic predicates dramatically speeds up computation of network reachability. On the average, AP Verifier is 3 orders of magnitude faster than an existing tool, Hassel in C. It also uses 2 to 3 orders of magnitude less memory than Hassel in C.