[ecoop-info] Annoucement: release of Java Typestate Checker

Antonio Ravara aravara at fct.unl.pt
Thu Sep 9 17:00:34 CEST 2021

We are glad to announce the first release of Java Typestate Checker 
(JaTyC [1]), a tool to statically check that class methods are called in 
a prescribed order, specified in a protocol file associated with that 
class. Our tool ensures that client code conforms to the specification, 
guaranteeing protocol compliance and completion.

Our teams, composed by Lorenzo Bacchiani and Mario Bravetti from the 
Bologna University (Italy), and by Marco Giunti, João Mota and António 
Ravara from the NOVA School of Science and Technology (Portugal), have 
joined forces and, building on previous work of each team, developed 
support for subtyping. In particular, this has been done by adapting a 
synchronous subtyping algorithm (with error detection) used in the 
general synchronous/asynchronous session subtyping tool presented in 
[2]. Our typestate checker can now safely handle polymorphic code, 
although in this first version in a limited way.

You can find a quick installation guide at 
https://github.com/jdmota/java-typestate-checker and further 
documentation at 

Feel free to send us feedback on your experience working with this tool.

Warm regards,
António (also on behalf of João, Lorenzo, Marco, and Mario)

[1] Mota, João, Marco Giunti, and António Ravara. “Java Typestate 
Checker”, in Proc. of COORDINATION 2021, LNCS 12717, Springer 2021

[2] Bacchiani, L., Bravetti, M., Lange, J., Zavattaro, G.: “A Session 
Subtyping Tool”, in Proc. of COORDINATION 2021, LNCS 12717, Springer 2021
Tool source files for Linux, Windows and OSx (and binaries for Windows 
and OSx).

More information about the ecoop-info mailing list