BPPChecker: An SMT-based Model Checker on Basic Parallel Processes

Due to the general undecidable results, verification of concurrent programs is a big challenge. Most existing verifiers adopt Petri net and its extensions based on abstraction and approximation as their verification models, which yet suffer from intractable complexity and are thus challenging to be efficient and complete. We choose Basic Parallel Process (BPP) , a subclass of Petri nets, as the backbone verification model for verifying concurrent programs due to its lower complexity. We propose BPPChecker, the first model checker for verifying a subclass of CTL on BPP. A constraint-based algorithm is given in which formulas are handled by SMT solver Z3. Our approach involves introducing a k -step semantics for the EG operator. By doing so, we reduce the problem of deciding the satisfiability of EG -formulas and EF 1 -formulas to the problem of deciding the satisfiability of linear integer arithmetic formulas. Besides, we encode the Actor Communicating System (ACS) , a program model for asynchronously communicating programs, to BPP. Experimental results show that BPPChecker performs more efficiently than the existing tools for a series of branching-time property verification problems of Erlang programs.