SAGA is a run-time verifier for single-threaded as well as multi-threaded Java programs. During the execution of a Java program, SAGA intercepts method calls and returns, and verifies that their stack traces conform to a specification defined previously by the user. What differentiates SAGA from other run-time checkers is that protocol-oriented and data-oriented properties can be combined in a single formalism.
SAGA has been developed by the Formal Methods (FM) group in close collaboration with the Software Analysis and Transformation (SWAT) group. It has been applied in the FP7 research project Envisage, in which a development framework for resource management in the cloud was created.
