Using Integer Programming to Verify General Safety and Liveness Properties

. Analysis of concurrent systems is plagued by the state explosion problem. We describe an analysis technique that uses necessary conditions, in the form of linear inequalities, to verify certain properties of concurrent systems, thus avoiding the enumeration of the potentially explosive number of reachable states of the system. This technique has been shown to be capable of verifying simple safety properties, like freedom from deadlock, that can be expressed in terms of the number of certain events occurring in a finite execution, and has been successfully used to analyze a variety of concurrent software systems. In this paper, we extend the technique to the verification of more complex safety properties that involve the order of events and to the verification of liveness properties, which involve infinite executions. Keywords: Concurrent systems, automated verification, integer programming, safety, liveness 1. Introduction Many concurrent systems can be modeled as a set of communic..