Overview
The Formally Verifiable Routing (FVR) project addresses a long-standing challenge in networking research -- bridging the gap between formal theories (for reasoning about protocol correctness) and actual implementations. One of our significant contributions is the FSR (Formally Safe Routing) toolkit [SIGCOMM'11 demo], that attempts to bridge this gap in the context of interdomain routing, by unifying research in routing algebras with recent advances in declarative networking to produce provably correct distributed implementations. Specifically, FSR automates the process of analyzing routing configurations expressed in algebra for safety (i.e. convergence) using SMT solvers, and automatically compiles routing algebra into declarative routing implementations. In addition to the FSR toolkit, the FVR project has also explored the use of theorem proving and rewriting logic techniques for verifying routing protcols. See our contributions and publications for more details.