Description: Verification of Java source code with respect to typestates. A typestate defines the object’s states, the methods that can be called in each state, and the states resulting from the calls. The tool statically verifies that when a Java program runs: sequences of method calls obey to object’s protocols; objects’ protocols are completed; null-pointer exceptions are not raised; subclasses’ instances respect the protocol of their superclasses.

Developed at: NOVA

Contacts: jd.mota@campus.fct.unl.pt

Available at: https://github.com/jdmota/java-typestate-checker