Scholarlink

We introduce a proof-producing symbolic execution tool for formal verification of P4 programs. The tool has been implemented using the interactive theorem prover HOL4 and results are proved sound with respect to the HOL4P4 formalisation of the P4 language. Most notably, this is a general tool for proving functional correctness that can be applied to entire real-world P4 programs.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Proof-Producing Symbolic Execution for P4

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Didrik Lundberg,
  • Roberto Guanciale,
  • Mads Dam

摘要

We introduce a proof-producing symbolic execution tool for formal verification of P4 programs. The tool has been implemented using the interactive theorem prover HOL4 and results are proved sound with respect to the HOL4P4 formalisation of the P4 language. Most notably, this is a general tool for proving functional correctness that can be applied to entire real-world P4 programs.