Zord is a bounded model checker for concurrent programs. We propose a new ordering consistency theory for concurrent program verification under sequential consistency, and we elaborate its theory solver.
P4-to-Boogie is an translator that translates P4 programs to Boogie programs automatically. We propose formal translation rules to ensure the correctness of the translation process. The translated results can be verified by the toolchain of Boogie.