Updated July 2009
Plural is a static protocol analysis tool for Java that I am developing with Nels Beckman. You can download the sources for Plural and find instructions on how to install it under Eclipse on Google Code. Plural is based primarily on papers published at OOPSLA 2007 and 2008. Experience with specifying and verifying Java code appeared at ECOOP 2009. My thesis provides a comprehensive description and evaluation of Plural's capabilities.
Updated July 2009
Crystal is a framework for static Java source code analyses inside the Eclipse IDE. Crystal supports "branch-sensitive" dataflow analyses that are aware of the outcome of conditional tests in the code, among other things. Crystal is open-source and available on Google Code together with an extensive wiki giving detailed descriptions of many of Crystal's features. Ciera Jaspan, Jonathan Aldrich, and myself gave a Crystal tutorial at the ECOOP 2009 summer school.
Posted February 2009
Together with several Masters students I worked on supporting typestate- based protocols between architectural components in the ArchJava programming language. We wrote a technical report describing our approach.
Updated January 2010
Based on my FSE'05 paper on lightweight object specification with typestates we are working on directly supporting typestates in the Java Modeling Language. We published our approach at SAVCBS '09.