Doenges, Ryan2024-04-052024-04-052023-08Doenges_cornellgrad_0058F_13892http://dissertations.umi.com/cornellgrad:13892https://hdl.handle.net/1813/114614164 pagesThis 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.endissertation or thesishttps://doi.org/10.7298/a0dy-4f33