Most of software I develop these days can be found in the tools section of gloss.

mil _ Multithreaded Intermediate Language

MIL is an intermediate language targeted at shared memory multiprocessors, where CPU cores synchronize via locks, acquired with a traditional get and set lock instruction. A polymorphic typing system enforces a strict protocol on lock usage, prevents race conditions and deadlocks.
Project's home page

mool _ Mini Object Oriented Language

MOOL is an OO language with support for concurrency, that allows programmers to specify class usage protocols as types. The specification formalizes (1) the methods available to clients, (2) the tests clients must perform on the values returned by methods, and (3) the existence of aliasing and concurrency restrictions, all of which depend on the object's state. Linear and shared objects are handled as a single category, allowing linear objects to evolve into shared ones.
Project's home page

congu _ CONtract-GUided system development

ConGu checks Java classes against property-driven algebraic specifications. It comprises a specification language; a language for defining refinement mappings between specifications and classes; a tool for replacing classes under test by automatically generated wrapper classes, annotated with contracts. The approach is currently tailored to Java and JML.
Project's home page


Bica is an extension of the Java language with session type annotations that describe the changes in object's interfaces. Session type specifications provide a flexible way to specify dymamic changes in object's interface. The session type is included in the source code of a type as a Java annotation; Bica verifies that clients of a class use it as specified by the session type.
Project's home page

tyco _ TYped Concurrent Objects

TyCO is an implicitly typed polymorphic concurrent language based on an extension of the asynchronous pi-calculus featuring first class objects, asynchronous messages and process definitions. Definitions allow, among other things, for object classes to be modeled. A type system assigns monomorphic types to variables and polymorphic types to definition identifiers. TyCO provides a clean model for a concurrent object-based language which combines the benefits of the formal framework of process calculi with the characteristics of Hewitt's actor system.
Project's home page