PLURAL: checking protocol compliance under aliasing. Enforcing compliance to API usage protocols is notoriously hard due to possible aliasing of objects through multiple references. In previous work we proposed a sound, modular approach to checking protocol compliance based on typestates that offers a great deal of flexibility in aliasing. In our approach, API protocols are defined based on typestates. Every reference is associated with a permission, and reasoning about permissions is appropriately conservative for the ”degree” of possible aliasing admitted by a permission. This paper describes Plural, a tool to automatically enforce typestate-based protocols using permissions in Java. API developers can specify protocols with simple annotations on methods and method parameters. A static flow analysis tracks permissions in code that uses specified APIs and issues warnings for possible protocol violations.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Gay, Simon J.; Gesbert, Nils; Ravara, António; Vasconcelos, Vasco T.: Modular session types for objects (2015)