SAT and SMT Based Model Checking of Concurrent Systems

摘要

We discuss model checking that uses a SAT (satisfiability) or SMT (satisfiability modulo theory) solver. The basic idea behind this model checking approach is to reduce the model checking problem to the satisfiability problem of a formula of some logic. Recent advances in SAT and SMT solvers make this particular approach sig-nificantly attractive. However, it does not work effectively in verification of concurrent systems, because the size of the formula blows up if the system has high concurrency. To overcome this challenge, we propose a new semantics for concurrent systems. The new semantics allows a compact formula representation of the behavior of concurrent systems. In this paper, we first introduce this new semantics and bounded model checking based on it, in the context of a general model of concurrent systems. Then we apply it to two specific concurrent system models, namely Petri nets and concurrent programs using unbounded integer variables.