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

TL;DR

BPPChecker is a novel SMT-based model checker designed for verifying CTL properties on Basic Parallel Processes, offering improved efficiency over existing Petri net-based tools, especially for concurrent program verification.

Contribution

It introduces the first model checker for a subclass of CTL on BPP, with constraint-based algorithms and SMT solving techniques tailored for BPP verification.

Findings

BPPChecker outperforms existing tools in efficiency.

It successfully verifies properties of Erlang programs modeled as ACS.

The approach reduces model checking problems to SMT satisfiability issues.

Abstract

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 based on Petri nets are difficult to be complete and efficient. Basic Parallel Process (BPP), as a subclass of Petri nets, can be used as a model for describing and verifying concurrent programs with lower complexity. We propose and implement BPPChecker, the first model checker for verifying a subclass of CTL on BPP. We propose constraint-based algorithms for the problem of model checking on BPPs and handle formulas by SMT solver Z3. For EF operator, we reduce the model checking of EF-formulas to the satisfiability problem of existential Presburger formula. For EG operator, we provide a k-step bounded semantics and reduce the model checking of EG-formulas to the satisfiability problem of linear integer arithmetic. Besides, we give Actor Communicating System (ACS) the over-approximation BPP-based semantics and evaluate BPPChecker on ACSs generated from real Erlang programs. Experimental results show that BPPChecker performs more efficiently than the existing tools for a series of branching-time property verification problems of Erlang programs.