SAT based verification of network data planes

Shuyuan Zhang, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

13 Scopus citations

Abstract

Formal verification has seen relatively less application in verifying computer networking infrastructure. This is in part due to the lack of clean layers of abstraction that enable design modeling and specification of correctness criteria. However, the recent move towards Software Defined Networking (SDN) provides a clean separation between a centralized control plane and a distributed data plane. This provides an opportunity to formally verify critical data plane properties. In this paper, we present a Boolean Satisfiability (SAT) based framework for data plane modeling and checking of key correctness criteria. This provides greater efficiency and/or greater coverage of properties when compared to other existing approaches.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings
Pages496-505
Number of pages10
DOIs
StatePublished - Nov 18 2013
Event11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013 - Hanoi, Viet Nam
Duration: Oct 15 2013Oct 18 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8172 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013
CountryViet Nam
CityHanoi
Period10/15/1310/18/13

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'SAT based verification of network data planes'. Together they form a unique fingerprint.

  • Cite this

    Zhang, S., & Malik, S. (2013). SAT based verification of network data planes. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Proceedings (pp. 496-505). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8172 LNAI). https://doi.org/10.1007/978-3-319-02444-8_43