Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking

摘要

In this paper we discuss reachability analysis for infinite-state systems in which states can be represented by a vector of integers. We propose a new algorithm for verifying reachability properties based on canonical representations of solutions to systems of linear inequations over integers instead of decision procedures for integer or real arithmetic. Experimental results demonstrate that problems in protocol verification which are beyond the reach of other existing systems can be solved completely automatically.