Polymorphic Fractional Permission Inference

Fractional permissions have recently received much attention for sound static reasoning about programs that rely on aliasing, but they are challenging to track automatically. This paper contributes an algorithm for proving permission-based assertions in a decid- able fragment of linear logic. Unlike previous work, our inference approach supports polymorphism over fractions. The paper also de- scribes our implementation of this algorithm as part of a tool, Plu- ral, which checks compliance to typestate-based protocols in Java code. We report Plural's performance on several benchmark pro- grams.