Hoare-Style Logic for Unstructured Programs. - Didrik Lundberg; Roberto Guanciale; Andreas Lindner; Mads Dam (SEFM, 2020)

HOL4P4: semantics for a verified data plane. - Anoud Alshnakat; Didrik Lundberg; Roberto Guanciale; Mads Dam; Karl Palmskog (EuroP4@CoNEXT, 2022)

Proof-Producing Symbolic Execution for P4. - Didrik Lundberg; Roberto Guanciale; Mads Dam (VSTTE, 2024)

HOL4P4: Mechanized Small-Step Semantics for P4. - Anoud Alshnakat; Didrik Lundberg; Roberto Guanciale; Mads Dam (Proc. ACM Program. Lang., 2024)