Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints

Chong Gao, Taolue Chen, Zhilin Wu

We identify difference-bound set constraints (DBS), an analogy of difference-bound arithmetic constraints for sets. DBS can express not only set constraints but also arithmetic con…