一句话：提出 P4b，将 P4 程序翻译为面向验证的中间表示 Boogie，并给出形式化翻译规则以保证正确性。
P4 是软件定义网络（SDN）数据平面的主流语言，但 P4 程序中的逻辑错误可能导致数据包处理异常，引发严重网络故障与信息泄露；且 P4 程序分支众多，正确性保障困难。现有 P4 形式验证研究缺乏基础工具链，其中间语言表达能力不足。为此，本文提出 P4b——一个从 P4 程序到面向验证的中间表示 Boogie 的高效翻译器。作者给出形式化翻译规则以保证翻译过程的正确性，翻译结果可利用 Boogie 工具链进行验证。作者在从 GitHub 收集的 170 个 P4 程序上开展实验，结果表明该翻译器实用且有效。工具与演示视频已公开。
P4 is a mainstream language for Software Defined Network (SDN) data planes. P4 is designed to achieve target-independent, protocol-independent, and configurable SDN data planes. However, logic errors may occur in P4 programs, resulting in improper packet processing, which may cause serious network errors and information disclosure. In addition, P4 programs contain many branches and thus are more challenging to ensure correctness. Formal verification is a powerful technique to verify the correctness of P4 programs. Unfortunately, current P4 verification studies lack basic toolchains, and their intermediate languages are not expressive enough. We present P4b, an efficient translator from P4 programs to Boogie, a verification-oriented intermediate representation. We provide formal translation rules to ensure the correctness of the translation process. The translated results can be verified by the toolchain of Boogie. We conducted experiments on 170 P4 programs collected from GitHub, and the experimental results demonstrate that our translator is useful and practical. The screencast is available at https://youtu.be/8_rEj3QFQeM. The tool is available at https://github.com/Invincibleyc/P4B-Translator.