Verification of computer switching networks: An overview

Shuyuan Zhang, Sharad Malik, Rick McGeer

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

17 Scopus citations

Abstract

Formal verification has seen much success in several domains of hardware and software design. For example, in hardware verification there has been much work in the verification of microprocessors (e.g. [1]) and memory systems (e.g. [2]). Similarly, software verification has seen success in device-drivers (e.g. [3]) and concurrent software (e.g. [4]). The area of network verification, which consists of both hardware and software components, has received relatively less attention. Traditionally, the focus in this domain has been on performance and security, with less emphasis on functional correctness. However, increasing complexity is resulting in increasing functional failures and thus prompting interest in verification of key correctness properties. This paper reviews the formal verification techniques that have been used here thus far, with the goal of understanding the characteristics of the problem domain that are helpful for each of the techniques, as well as those that pose specific challenges. Finally, it highlights some interesting research challenges that need to be addressed in this important emerging domain.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Proceedings
Pages1-16
Number of pages16
DOIs
StatePublished - Nov 6 2012
Event10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 - Thiruvananthapuram, India
Duration: Oct 3 2012Oct 6 2012

Publication series

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

Other

Other10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012
CountryIndia
CityThiruvananthapuram
Period10/3/1210/6/12

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Verification of computer switching networks: An overview'. Together they form a unique fingerprint.

Cite this