Add CBMC and JBMC
Both model-checkers use the CPROVER framework. CBMC supports C (see
http://www.cprover.org/cbmc/) and offers partial support for SystemC. JBMC is
the Java frontend of CPROVER and supports Java bytecode analysis.
Both are developed as open-source tools by Diffblue ltd.
@@ -47,6 +47,7 @@ Also check out the sister project, [awesome-dynamic-analysis](https://github.com
## C/C++
+* [CBMC](http://www.cprover.org/cbmc/) - bounded model-checker for C programs, user-defined assertions, standard assertions, several coverage metric analyses
* [clang-tidy](http://clang.llvm.org/extra/clang-tidy/) - clang static analyser
* [CMetrics](https://github.com/MetricsGrimoire/CMetrics) - Measures size and complexity for C files
* [CodeSonar from GrammaTech](https://www.grammatech.com/products/codesonar) :copyright: - Advanced, whole program, deep path, static analysis of C and C++ with easy-to-understand explanations and code and path visualization.
@@ -177,6 +178,7 @@ Also check out the sister project, [awesome-dynamic-analysis](https://github.com
* [Hopper](https://github.com/cuplv/hopper) - A static analysis tool written in scala for languages that run on JVM
* [HuntBugs](https://github.com/amaembo/huntbugs) - Bytecode static analyzer tool based on Procyon Compiler Tools aimed to supersede FindBugs.
* [JArchitect](https://www.jarchitect.com) :copyright: - Measure, query and visualize your code and avoid unexpected issues, technical debt and complexity.
+* [JBMC](http://www.cprover.org/jbmc/) - bounded model-checker for Java (bytecode), verifies user-defined assertions, standard assertions, several coverage metric analyses
* [NullAway](https://github.com/uber/NullAway) - Type-based null-pointer checker with low build-time overhead; an [Error Prone](http://errorprone.info/) plugin
* [OWASP Dependency Check](https://www.owasp.org/index.php/OWASP_Dependency_Check) - Checks dependencies for known, publicly disclosed, vulnerabilities.
* [Spoon](https://github.com/INRIA/spoon) - Library to write your own static analyses and architectural rule checkers for Java. Can be integrated in Maven and Gradle.
