Skip to Content

Static Analysis Tools

Posted on 2 mins read

This page is a random-ish collection of links to static analysis resources.

Formal verification tools

OpenJML OpenJML is a toolset for static and dynamic checking of JML (Java) assertions. Uses a variety of SMT automatic theorem provers, default configuration uses Microsoft’s Z3 prover. https://github.com/Z3Prover/z3

KeY Project KeY is a verification system that uses an interactive theorem prover to verify Java/JML and other languages. In theory an interactive theorem prover can be much more powerful than an automatic one (e.g., Z3).

Spin Spin is a extremely popular and long-lasting and well-engineered model checker.

Ad-hoc, bug pattern, style checkers, and other tools

A curated list of available tools for many programming languages and frameworks The organization level also has other repos, including a curated list of dynamic analysis tools.

Github also has some topic tags worth exploring: static-analysis, static-code-analysis, dynamic-analysis, linter, and many more!

Facebook has an interesting C/C++/C# tool they use internally: Infer

An interesting article pointing to Google and FB using ananlysis tools

A Google created Java analysis tool: ErrorProne

OWASP is security-oriented

Source_Code_Analysis_Tools

Wikipedia:static_tools is a decent place to start, but perhaps overwhelming.

SpotBugs is the successor of FindBugs (Java bug pattern detector & plug-in framework).

PMD is a fairly successful code analysis tool (somewhat cross language); includes clone detector.

CppCheck is a C/C++ code checker. Quite useful.

ESLint is a Javascript code analysis tool (“lint” was the original name of an old C code analysis tool, and several tools continue the tradition of using “lint” in their names; the idea is a tool that can find “lint”, which is tiny stuff).

PyLint is the main Python Linter (code analyzer).

GitHub:code-quality shows all the github-integrated tools that do some sort of code analysis for your project.

Codacy is one github-integrated professional static analysis tool that is free for open source github projects.

MS placeholder for referencing multiple MS public projects for code analysis. Hard to tell if it is up to date.

someone’s attempt to catalog many code analysis tools out there. It is just a catalog, not a tool itself.

DeepScan is an example profession free-for-open-source Javascript analysis tool.

Miscellaneous

PySAT and SatisPy are two python packages that provide interfaces to off-the-shelf boolean satisfiability checkers. Boolean satisfiability is the bedrock of many verification ideas.

SimpleSATExample presents the ideas of boolean satisfiability by showing a simple implementation in Python. Nice tutorial but very inefficient – for REAL SAT problems use the interface packages with a REAL SAT solver!