Relevant Links

The items in the list below link to information relevant to static analysis and the annotations project as a whole. For more information about specific tools, look here.

Technical Reports:

Specifications and Extended Static Checking for LLVM
C Library annotations in ACSL for Frama-C: experience report
Annotating public bugs with ACSL: Experience report

Specification Languages:

Wikipedia's compilation

Formal Methods:

Formal Methods Europe and its tools list
Formal Methods Wikia

Formal Methods:

Wikipedia's page on static program analysis and tools

Note: This page contains an extensive list of static analysis tools, ranging from simple syntax checking to sophisticated inter-procedural analyses. Some of the listed items are out-of-date or no longer supported.

NIST's SAMATE evaluation site
Owasp's list of source code analysis tools
With a focus on security

Model Checking Tools:

Wikipedia's list of model checking tools

Requirements Management:

Requirements are the original source of formal specifications, although not all requirements are formalized. Eventually, we would like to see a connection built between requirements management tool sand formal verification or static analysis tools.

List of requirements management tools (from 2013)

Other Commentary:

Gerard Holzmann's notes, primarily about C checkers
Source Code Analysis Tools: How to Choose and Use Them
Jon Carmac recounts his conversion and experience with static analysis

On LinkedIn:

Static Code Analysis
Formal Methods: Specification, Verification, TCG
Software Development with Formal Methods
Software Model Checking
Formal Methods Europe