FSR: Formal analysis and implementation toolkit for safe inter-domain routing

Yiqing Ren, Wenchao Zhou, Anduo Wang, Limin Jia, Alexander J.T. Gurney, Boon Thau Loo, Jennifer Rexford

Research output: Contribution to journalArticlepeer-review

3 Scopus citations


We present the demonstration of a comprehensive toolkit for analyzing and implementing routing policies, ranging from high-level guidelines to specific router configurations. Our Formally Safe Routing (FSR) toolkit performs all of these functions from the same algebraic representation of routing policy. We show that routing algebra has a very natural translation to both integer constraints (to perform safety analysis using SMT solvers) and declarative programs (to generate distributed implementations). Our demonstration with realistic topologies and policies shows how FSR can detect problems in an AS's iBGP configuration, prove sufficient conditions for BGP safety, and empirically evaluate convergence time.

Original languageEnglish (US)
Pages (from-to)440-441
Number of pages2
JournalComputer Communication Review
Issue number4
StatePublished - Aug 15 2011

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Networks and Communications


  • Formal verification
  • Formally safe routing
  • Safety analysis


Dive into the research topics of 'FSR: Formal analysis and implementation toolkit for safe inter-domain routing'. Together they form a unique fingerprint.

Cite this