Abstract
dc:description.abstractThis dissertation gives semantics to P4, a domain-specific language for describing packet processing in packet-switched computer networks. Additionally it describes verification tools for checking the equivalence of P4 programs. These verifiers can be used to check that a P4 compiler has not introduced bugs into programs while optimizing them. The verification methodology combines manual proof in an LCF-style proof assistant with automatic decision procedures that rely on SAT/SMT solvers for a compact trusted computing base.
Degree
thesis:*- Name thesis:degree_name
- Ph. D., Computer Science
- Level thesis:degree_level
- Doctor of Philosophy
- Discipline thesis:degree_discipline
- Computer Science
- Grantor
- Cornell University
- Year dc:date.issued
- 2023
Author and committee
dc:creator, dc:contributor.*- Author dc:creator
-
- Doenges, Ryan
- Committee members dc:contributor.committeemember
-
- Van Renesse, Robbert
- Peraino, Judith
- Morrisett, John
Rights
- Language dc:language.iso
- en
Identifiers
dc:identifier.*- Dc Identifier Other
-
ProQuest Submission ID: 13892
ProQuest Publication ID: 30575725 - OAI identifier oai:identifier
- oai:ecommons.cornell.edu:1813/114614