Symbolic representations for integer sets in automated verification

A popular method for verification of temporal properties of transition systems is model checking, a systematic exploration of the state space of a system. Explicit representation of states i.e., sets of values of the variables, has been proven inefficient for large and complex systems. For such systems symbolic representations appear to be quite successful. In this work we study symbolic representations for states described by linear arithmetic constraints. We consider two cases: finite and infinite state spaces, depending on whether the variables of the system are bounded or unbounded, respectively. We propose construction algorithms for efficient symbolic representations for linear arithmetic constraints and analyze the complexity of various operations used in model checking. We also implemented these algorithms and used them to verify a wide range of systems such as monitor specifications and mutual exclusion protocols. We experimentally compare the performance of our techniques to other alternative approaches.