A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
This work provides a decision procedure for a specific logic extension, allowing automated verification of systems involving set intervals, which is incremental but useful for formal methods in domains like software verification.
The paper extends a decision procedure for finite sets with cardinality constraints to include finite integer intervals, enabling automated reasoning about quantifier-free formulas involving set operators like minimum and maximum. The implementation in the {log} tool successfully discharges all invariance lemmas in an elevator algorithm case study.
In this paper we extend a decision procedure for the Boolean algebra of finite sets with cardinality constraints ($\mathcal{L}_{\lvert\cdot\rvert}$) to a decision procedure for $\mathcal{L}_{\lvert\cdot\rvert}$ extended with set terms denoting finite integer intervals ($\mathcal{L}_{[\,]}$). In $\mathcal{L}_{[\,]}$ interval limits can be integer linear terms including \emph{unbounded variables}. These intervals are a useful extension because they allow to express non-trivial set operators such as the minimum and maximum of a set, still in a quantifier-free logic. Hence, by providing a decision procedure for $\mathcal{L}_{[\,]}$ it is possible to automatically reason about a new class of quantifier-free formulas. The decision procedure is implemented as part of the $\{log\}$ tool. The paper includes a case study based on the elevator algorithm showing that $\{log\}$ can automatically discharge all its invariance lemmas some of which involve intervals.