Author
Marco Chiesa presented our recent results from the SEMLA projectto the SMARTNESS consortium, a research collaboration among multiple Brazilian universities, organizations, and Ericsson.
Author
Changjie Wang and Mariano Scazzariello have attended ACM CoNEXT in Los Angeles this week! Our work, NetConfEval, has been shortlisted among the three top papers in the conference out of 38 accepted papers (and 250 submitted ones)! Congratulations to the team!
Enjoy the presentation talk from Changjie Wang:
Author
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.
GitHub code: link
Paper PDF: link
Authors: Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam
Author
In a recent paper, we show how to formally verify P4 code using the interactive theorem prover (ITP) HOL4. The method creates an end-to-end proof entirely inside the logic of the ITP, and is applicable to real P4 programs by using the import tool of HOL4P4. To gain efficiency when symbolically executing large programs, multiple types of semantics are used, with proofs of soundness with respect to the standard semantics enabling the composition of their results.
This tool can be used by SEMLA in the future to formally verify that P4 code generated by LLMs respects certain program specifications.
Authors: Didrik Lundberg, Roberto Guanciale, Mads Dam.
Author
Marco Chiesa presented the recent results from the CoNEXT paper at NVidia Research.
