P4AIG: Circuit-Level Verification of P4 Programs

Mohammad A. Noureddine, Amanda Hsu, Matthew Caesar, Fadi A. Zaraket, William H. Sanders

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

Abstract

In this work, we set out to develop P4 AIG, a tool for the static verification of programmable data planes using sequential circuit analysis. P4 AIG targets P4 programs by treating them as hardware pipelines rather than software programs. P4 AIG allows for the circuit-level treatment of P4 programs, a feature not available for traditional software verification techniques. We believe that P4 AIG will exploit the nature of P4 programs to achieve higher scalability in verification.

Original languageEnglish (US)
Title of host publicationProceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages21-22
Number of pages2
ISBN (Electronic)9781728130286
DOIs
StatePublished - Jun 2019
Event49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019 - Portland, United States
Duration: Jun 24 2019Jun 27 2019

Publication series

NameProceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019

Conference

Conference49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019
Country/TerritoryUnited States
CityPortland
Period6/24/196/27/19

Keywords

  • data plane programs
  • software defined networks
  • verification

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Information Systems
  • Information Systems and Management
  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'P4AIG: Circuit-Level Verification of P4 Programs'. Together they form a unique fingerprint.

Cite this