Bounded Model Checking of Concurrent Systems with Unbounded Integer Variables

We discuss bounded model checking that uses a Satisfiability Modulo Theory (SMT) 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 SMT solvers make this particular approach significantly 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, we adopt a different encoding for concurrent systems from the standard one. This encoding allows a compact formula representation of the behavior of concurrent systems. In this paper, we focus our attention on the verification of concurrent systems with unbounded integer variables and show how the new encoding helps improve the performance of model checking.