Explanation: The developer annotates multi- threaded code to declare desired thread safety properties. Tool (compiler option) assures that the policies are enforced.
Vulnerabilities addressed: Addresses race conditions and deadlocks.
Developer resources required: Requires programmers capable of developing correct annotations, and access to a compiler capable of processing them.
Evaluator resources required: Requires the ability to determine that appropriate annotations have been made (manual) and that all the software was processed with the appropriate compiler and options (or recompile it) and the ability to review the specified safety policies.