Where Static Analysis is Less Helpful


Determinism: Persistent route oscillation

Safety: Policy disputes [Griffin 2001]

We suggest protocol modifications to 
make BGP more verifiably correct.