Research Preparation Exam: Hongkun Yang, GDC 6.816

Contact Name: 
Lydia Griffith
Jun 27, 2013 3:00pm - 4:00pm

Research Preparation Exam: Hongkun Yang

Date: June 27, 2013
Time: 3:00pm - 4:00pm
Location: GDC 6.816
Committee members: E. Allen Emerson, Mohamed G. Gouda,  and Simon S. Lam (chair)

Title: 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. The
use of atomic predicates dramatically speeds up computation of
network reachability. 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.