- Clang Static Analyzer: finds bugs in C, C++, and Objective-C code
- jCUTE: Java concolic unit testing
- Atomic Set Inferencer, its github (FUSC, Java/Shell): for automatically inferring atomic sets, a synchronization mechanism in which the programmer specifies the groups of data that must be accessed as a unit (UIUC)
- SOTER (FUSC): extensible static analysis and transformation tool that facilitates safe yet efficient message passing in actor programs (UIUC)
- Splint (was: LCLint) (GPL-2, C): Secure programming Lint for static C checking (Univ. Virginia)
- Jakstab, its hg (GPL-2, Java): Abstract Interpretation-based, integrated disassembly and static analysis framework for designing analyses on executables and recovering reliable control flow graphs (TU Munchen, TU Darmstadt)
- SLAM (Microsoft Research)
- Jahob: Java static contract analysis (EPFL)
- KLEE (C, LLVM): Symbolic virtual machine built on top of the LLVM compiler infrastructure. Provides unassisted and automatic generation of high-coverage tests.
- SOOT (LGPLv2.1, Java): a framework for analyzing and transforming Java and Android applications
- Frama-C (LGPLv2, C): an extensible and collaborative platform dedicated to source-code analysis of C software
- infer (BSD-3, OCaml): Infer is a static analysis tool for Java, Objective-C and C. The documentation is at https://fbinfer.com/. (Facebook)
- Gravy (LGPL, Java): static checker for Boogie programs. Similar to a deductive verifier, such as Boogie, it checks a boogie program one procedure at a time. Integrated in Bixie
- Bixie (MIT, Java): inconsistent code detection for Java, integrates Gravy (SRI CSL)
- Calysto (?, ?): static checker for general purpose code, does not require users to write interface specifications and pre/post-conditions. Calysto checks pointer properties and user provided assertions. (Google)
semgrep(LGPL-2.1, Python/OCaml): pattern-based static analysis, with patterns that resemble code excerpts