Annotation Tools and Use

Annotation Tools and Use

The chart below lists analysis and model-checking tools that we have investigated. There is an emphasis on tools that work with source code or extract models from source code, and use a defined annotation language (or could be embellished to do so). If you have suggestions of other relevant tools to investigate, please let us know.

Tool Type Source Language Annotation Language Current Status Last Update
Checker framework Static analysis tool with keyword annotations. Java Java annotation keywords Open-source, current. 2016
CodeContracts Static analysis tool with a full annotation language. Has VisualStudio support. .NET languages e.g. C# expressions Available commercially, has ongoing development and support. 2016
Dafny Static analysis tool with a full annotation language. Dafny Dafny Research tool with limited/no commercial support. 2016
Eiffel Static analysis tool with a full annotation language. Originally designed for runtime checking; static checking with AutoProof and Boogie. Eiffel Eiffel Available commercially, has ongoing development and support. 2016
ESC/Java2, ESC/Java Static analysis tool with a full annotation language. ESC/Java works only with early versions of Java and JML; ESC/Java 2 is available but only is for Java 4. Java JML No longer available. 2008
FindBugs Static analysis tool with keyword annotations (no annotation language support). Mostly doesn't use annotations, but does for nullity checking. Java Java annotation keywords Open-source, current. 2015
Frama-C Static analysis tool with a full annotation language C ACSL Open-source, current. 2016
KeY Static analysis tool with a full annotation language. Java JML or OCL Open-source, current. 2014
Leon Static analysis tool with a full annotation language. Scala Scala expressions Research tool with limited/no commercial support. 2015
OpenJML Static analysis tool with a full annotation language. Java JML Incomplete prototype under active development. 2016
SPARK Static analysis tool with a full annotation language SPARK Ada SPARK contracts (based on using Ada 2012 aspects in the latest version of the language) Open-source, with commercially available support and maintenance; under active development 2016
Spec# Static analysis tool with a full annotation language. Has VisualStudio integration. Spec# (C#) Spec# Research tool with limited/no commercial support. Not under current development. 2011
Spin +Modex Model-checker that works directly on source code or has a translation tool to extract a model from source code. C PROMELA (model language) Open-source, current. 2016
WhyR An annotation tool for LLVM IR. Adds function contracts and assertions to LLVM. LLVM IR LLVM metadata Open-source, current. A part of the Annotations For All project. 2016

Contribute to the Project

On GitHub:

Repository
Releases
Issue Tracker