{"id":40,"date":"2024-10-31T22:58:57","date_gmt":"2024-10-31T21:58:57","guid":{"rendered":"https:\/\/www.kth.se\/blogs\/semla\/?p=40"},"modified":"2024-10-31T22:58:57","modified_gmt":"2024-10-31T21:58:57","slug":"p4-semantics-presented-at-oopsla-2024","status":"publish","type":"post","link":"https:\/\/www.kth.se\/blogs\/semla\/2024\/10\/p4-semantics-presented-at-oopsla-2024\/","title":{"rendered":"P4 semantics presented at OOPSLA 2024"},"content":{"rendered":"<p>Last week, the HOL4P4 formalisation of the P4 language was presented at the OOPSLA conference. HOL4P4 is a model of the P4 language written in the interactive theorem prover HOL4, which differs from existing work by its efficient and judicious scoping mechanism and fine-grained, incremental semantic style. These design choices make it easier to construct analysis tools and model concurrent phenomena using HOL4P4. The HOL4P4 formal semantics has since been used to create a practical theorem-grade verification tool for P4, which has already been presented at VSTTE.<\/p>\n<p>GitHub code: <a class=\"c-link\" href=\"https:\/\/github.com\/kth-step\/HOL4P4\/tree\/OOPSLA2024\" target=\"_blank\" rel=\"noopener noreferrer\" data-stringify-link=\"https:\/\/github.com\/kth-step\/HOL4P4\/tree\/OOPSLA2024\" data-sk=\"tooltip_parent\">link<\/a><br \/>\nPaper PDF:\u00a0<a class=\"c-link\" href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649819\" target=\"_blank\" rel=\"noopener noreferrer\" data-stringify-link=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649819\" data-sk=\"tooltip_parent\">link<\/a><\/p>\n<p>Authors: Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Last week, the HOL4P4 formalisation of the P4 language was presented at the OOPSLA conference. HOL4P4 is a model of the P4 language written in the interactive theorem prover HOL4, which differs from existing work by its efficient and judicious scoping mechanism and fine-grained, incremental semantic style. These design choices make it easier to construct &hellip; <a href=\"https:\/\/www.kth.se\/blogs\/semla\/2024\/10\/p4-semantics-presented-at-oopsla-2024\/\" class=\"more-link\">Continue reading<span class=\"screen-reader-text\"> &#8220;P4 semantics presented at OOPSLA 2024&#8221;<\/span><\/a><\/p>\n","protected":false},"author":1312,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"inline_featured_image":false,"footnotes":""},"categories":[1],"tags":[],"class_list":["post-40","post","type-post","status-publish","format-standard","hentry","category-okategoriserat"],"jetpack_featured_media_url":"","_links":{"self":[{"href":"https:\/\/www.kth.se\/blogs\/semla\/wp-json\/wp\/v2\/posts\/40","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.kth.se\/blogs\/semla\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.kth.se\/blogs\/semla\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.kth.se\/blogs\/semla\/wp-json\/wp\/v2\/users\/1312"}],"replies":[{"embeddable":true,"href":"https:\/\/www.kth.se\/blogs\/semla\/wp-json\/wp\/v2\/comments?post=40"}],"version-history":[{"count":1,"href":"https:\/\/www.kth.se\/blogs\/semla\/wp-json\/wp\/v2\/posts\/40\/revisions"}],"predecessor-version":[{"id":41,"href":"https:\/\/www.kth.se\/blogs\/semla\/wp-json\/wp\/v2\/posts\/40\/revisions\/41"}],"wp:attachment":[{"href":"https:\/\/www.kth.se\/blogs\/semla\/wp-json\/wp\/v2\/media?parent=40"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.kth.se\/blogs\/semla\/wp-json\/wp\/v2\/categories?post=40"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.kth.se\/blogs\/semla\/wp-json\/wp\/v2\/tags?post=40"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}