Projects

AutoMerge aims to resolve merge conflicts that cannot be resolved by existing structured merge approaches.

paper

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.

RSLearn is a data-driven non-termination analysis tool based on Boogie and ICE learning algorithm.