Detail

Gluon — Verification of Contracts for Concurrency

This tool verifies Java programs using Soot, a Java static analysis framework.
This framework directly analyses Java bytecode, allowing compiled programs
to be verified without requiring access to its source code, which often is not available,
specially for third-party libraries.

The tool was developed by Diogo Sousa during his master thesis under supervision of João Lourenço and Carla Ferreira.