Bica is an extension of the Java language that enables the verification of Java programs against a session type specification. This specification represents the changes in the interface of an object. In Java, the interface of an object is the set of methods declared in the object's class, with visibility taken into account. Session type specifications provide a more flexible way to specify changes in the interface of an object.
The session type is included in the source code for a class as a Java annotation. Types are extended with session type information, and Bica verifies that clients of a class use it as specified by the session type. Bica is implemented using the Polyglot framework, as an extension of the jl5 language extension. That is, it supports Java 5 source code.
The theoretical backgrounds of Bica are the work on Session Types and Dynamic Interfaces. Although not fully implemented, Bica was designed to integrate seamlessly the verification of distributed communication programs too. The ideas and algorithms implemented in Bica can be found in the Publications section.
Bica is the result of close cooperation between researchers from Universidade de Lisboa, Universidade Nova de Lisboa and University of Glasgow. You can find the current team at the Team section.