Plural is a sound modular typestate checking tool for Java that employs fractional permissions to allow flexible aliasing control. Plural supports atomic blocks to check concurrent programs. Typestates can be used to define object protocols with finite state machines; Plural's protocols can involve multiple interacting objects. Plural is developed by Nels Beckman and Kevin Bierhoff at Carnegie Mellon University based on their papers published together with Jonathan Aldrich at OOPSLA 2007 and 2008 and elsewhere.
The tool is an Eclipse plugin that relies on the Crystal static analysis framework. It also uses the Antlr parser generator, which is released under the BSD license. Some Plural test code comes from the Jgroups project, which is released under the LPGL v2.1 license.
Latest News
- We've added a screen capture demo of Sync-or-Swim to Vimeo here. This has the added benefit of actually having readable text. (Use HD, and watch in fullscreen mode.)
- There is now a demo of Plural on YouTube. As part of Kevin's Thesis, a screen capture, with audio, was recorded. You can check it out here.
- The "Fiddle" object protocol visualization no longer depends on any outside plug-ins, so it should be much easier to install. There will be an updated pushed out soon.
- We wrote a paper on Plural's internals and in particular, how it tracks permissions in Java. Check it out!
- We changed the update site URL to avoid confusion with the Crystal update site, see Installation.
- A new wiki page, on GettingStarted should help the new PLURAL user. Please post any questions as comments to this page, and we'll get back to you ASAP!
- We have finally posted the PLURAL annotations which are needed to run our analysis. Find out more on the Annotations page.
- Nels has posted a series of NIMBY examples that are in the PLURAL test project and discussed on this page.
Photo by massenpunkt.
