BPPChecker: An SMT-based Model Checker on Basic Parallel Processes(Full Version)

Ying Zhao, Jinhao Tan, Guoqiang Li

Program verification on concurrent programs is a big challenge due to general undecidable results. Petri nets and its extensions are used in most works. However, existing verifiers…