{"id":{"repo_id":"cornell","oai_identifier":"oai:ecommons.cornell.edu:1813/114614"},"canonical_url":"https://search.dev.ndltd.org/etd/cornell/oai:ecommons.cornell.edu:1813/114614","repository":{"repo_id":"cornell","name":"Cornell University","base_url":"https://ecommons.cornell.edu/server/oai/request"},"display":{"title":"Programming Language Foundations for Packet Processing","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_html":"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_has_math":false,"creators":["Doenges, Ryan"],"institution":"Cornell University","degree_name":"Ph. D., Computer Science","degree_level":"Doctor of Philosophy","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":["Van Renesse, Robbert","Peraino, Judith","Morrisett, John"],"year":2023,"date_issued":"2023-08","date_published":"2023-08","updated_at":"2026-07-24T01:49:08Z","subjects":[],"languages":["en"],"rights":[],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier.doi","label":"DOI","values":["https://doi.org/10.7298/a0dy-4f33"],"render_values":[{"text":"https://doi.org/10.7298/a0dy-4f33","href":"https://doi.org/10.7298/a0dy-4f33","code":true}]},{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["ProQuest Submission ID: 13892","ProQuest Publication ID: 30575725"],"render_values":[{"text":"ProQuest Submission ID: 13892","href":null,"code":true},{"text":"ProQuest Publication ID: 30575725","href":null,"code":true}]}]},"links":{"outbound_url":"https://hdl.handle.net/1813/114614","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.committeemember","label":"Committee Member","values":["Van Renesse, Robbert","Peraino, Judith","Morrisett, John"]},{"key":"dc:creator","label":"Author","values":["Doenges, Ryan"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2024-04-05T18:46:28Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2024-04-05T18:46:28Z"]},{"key":"dc:date.issued","label":"Date","values":["2023-08"]},{"key":"dc:type","label":"Dc Type","values":["dissertation or thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Doctor of Philosophy"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph. D., Computer Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Cornell University"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.doi","label":"DOI","values":["https://doi.org/10.7298/a0dy-4f33"]},{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["ProQuest Submission ID: 13892","ProQuest Publication ID: 30575725"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1813/114614"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["164 pages"]},{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format.mimetype","label":"Dc Format Mimetype","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Programming Language Foundations for Packet Processing"]}]}],"canonical_facts":{"dc:contributor.committeemember":["Van Renesse, Robbert","Peraino, Judith","Morrisett, John"],"dc:creator":["Doenges, Ryan"],"dc:date.accessioned":["2024-04-05T18:46:28Z"],"dc:date.available":["2024-04-05T18:46:28Z"],"dc:date.issued":["2023-08"],"dc:description":["164 pages"],"dc:description.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."],"dc:format.mimetype":["application/pdf"],"dc:identifier.doi":["https://doi.org/10.7298/a0dy-4f33"],"dc:identifier.other":["ProQuest Submission ID: 13892","ProQuest Publication ID: 30575725"],"dc:identifier.uri":["https://hdl.handle.net/1813/114614"],"dc:language.iso":["en"],"dc:title":["Programming Language Foundations for Packet Processing"],"dc:type":["dissertation or thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Doctor of Philosophy"],"thesis:degree_name":["Ph. D., Computer Science"],"thesis:institution_name":["Cornell University"]},"updated_at":"2026-07-24T01:49:08Z"}