Abstract
Resource sharing is a fundamental phenomenon in concurrent programming, where multiple threads hold permissions to access a common resource. Verification logics must therefore capture permission ownership and transfer. A common approach is to use rational numbers in $(0,1]$ as permissions, where 1 represents full permission and fractional values represent partial ownership. However, rational permissions are not a natural fit for separation logic, as they weaken its essential notion of disjointness. We propose a general logical framework that supports permission reasoning in separation logic while preserving disjointness. Our framework enables sophisticated verification tasks such as induction over heap finiteness within the object logic, biabductive inference, and proofs of precision for recursive predicates within the object logic. We introduce scaling separation algebras , a compositional extension of separation algebras, to model our logic and construct a concrete semantic model. We also developed the ShareInfer tool to benchmark our techniques.