2026-09-18T21:06:58Zhttps://ecommons.cornell.edu/server/oai/requestoai:ecommons.cornell.edu:1813/1146142026-05-15T19:43:53Zcom_1813_35col_1813_47
Doenges, Ryan
Foster, John
Van Renesse, Robbert
Peraino, Judith
Morrisett, John
2024-04-05T18:46:28Z
2024-04-05T18:46:28Z
2023-08
ProQuest Submission ID: 13892
ProQuest Publication ID: 30575725
https://hdl.handle.net/1813/114614
https://doi.org/10.7298/a0dy-4f33
16219276
164 pages
This 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.
en
Programming Language Foundations for Packet Processing
dissertation or thesis
https://newcatalog.library.cornell.edu/catalog/16219276
application/pdf
Computer Science
Cornell University
Doctor of Philosophy
Ph. D., Computer Science
https://hdl.handle.net/1813/59810.2
Publication
Cornell Theses and Dissertations
Doenges, Ryan
5893a6ea-7af3-41d7-abc6-04bcd26ab5df
open.access
open.access
<Publication xmlns="https://www.openaire.eu/cerif-profile/1.1/" id="0cbdd899-c899-423b-bc2f-5502366b2766">
<Type xmlns="https://www.openaire.eu/cerif-profile/vocab/COAR_Publication_Types">http://purl.org/coar/resource_type/c_1843</Type>
<Language>en</Language>
<Title>Programming Language Foundations for Packet Processing</Title>
<PublishedIn>
<Publication>
</Publication>
</PublishedIn>
<PublicationDate>2023-08</PublicationDate>
<DOI>https://doi.org/10.7298/a0dy-4f33</DOI>
<Authors>
<Author>
<DisplayName>Doenges, Ryan</DisplayName>
<Affiliation>
<OrgUnit>
</OrgUnit>
</Affiliation>
</Author>
</Authors>
<Editors>
</Editors>
<Publishers>
<Publisher>
<OrgUnit />
</Publisher>
</Publishers>
<Abstract>This 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.</Abstract>
<Access xmlns="http://purl.org/coar/access_right"
>
</Access>
</Publication>