| Tool Name |
Platform |
Commercial/ Research |
Comments |
| Klocwork |
C/C++/Java |
C |
Commercial analysis tool that
can find null dereferences, buffer
over/underruns, memory errors, format string
vulnerabilities, etc. A free demo of Klocwork Solo is available.
|
| Fluid/SureLogic JSure |
Java |
C |
Commercial analysis tool that
finds concurrency problems using static and dynamic analysis. This is
the tool that was described in class. The instructor can get you a tool
license.
|
| Microsoft Pex |
.NET languages |
C/R |
High-quality research tool
released by Microsoft; aids in testing and test generation.
|
| Parasoft |
C/C++/Java/.NET |
C |
Commercial test generation tool. Also checks "coding rules." |
| Checkmarx |
Java/.NET/PHP/C/C++/VB/Ruby/JavaScript/Perl |
C |
Static analysis, focused on security |
| Eclat |
Java |
R |
Automatically generates test
inputs for a Java program |
| Purify | C, C++, Java |
C |
Detects memory errors in C/C++
programs at runtime, or
debugs garbage-collection related problems in Java |
| Java PathFinder | Java |
R |
Model checker for Java programs,
finds protocol-related errors |
| Zing | C# |
R |
Model checker for C# programs, finds protocol-related errors |
| FindBugs | Java |
R |
Collection of unsound bug
detectors for Java. |
| Daikon | C, Java |
R |
Tool for dynamically detecting likely invariants in Java and C/C++ programs. |
| BOOP | C |
R |
Model checker for C programs,
modeled after SLAM. |
| Reflexion Models | Java |
R |
A tool for reverse engineering
programs |
| Microsoft's Standard
Annotation Language |
.Net |
C |
Annotation-based static analysis
for buffer overflows and other vulnerabilities. Part of Visual Studio 2005 team edition; the instructor has a trial copy available for your experimentation (contact the instructor). |
| Rigi | C |
R |
A tool for reverse engineering programs |
| PMD | Java |
R |
Finds design-related errors |
| JLint | Java |
R |
Finds bugs in Java |
| Bandera | Java |
R |
Model checker for Java, finds
protocol-related errors |
| Lackwit | R |
Designed to aid reverse engineering or restructuring tasks | |
| Splint (formerly LCLint) | C |
R |
Finds security vulnerabilities and coding mistakes |
| EclipsePro Audit
and Test |
Java |
C |
EclipsePro Audit - Finds style
violations and other Java issues (e.g. rules from Effective Java book) EclipsePro Test - test generation and coverage tool |
| VeriSoft |
C/C++ on Unix |
R |
Model checker for concurrent
Unix programs |
| Lattix
LDM |
C/C++/Java |
C |
Supports dependency analysis
through Design Structure Matrices |
| FxCop |
.Net |
C |
Checks coding style and
guidelines with an eye towards performance |
| DataFactory |
Windows |
C |
Generates test data in a database |
| JProfiler |
Java |
C |
Performance evaluation tool,
including memory usage and time profiling |
| Coverity |
C, C++ |
C |
Commercial analysis tool that
can find null dereferences, buffer over/underruns, memory and
concurrency errors, format string vulnerabilities, etc.
Reports released by aGreement with
Coverity. |
| Grammatech CodeSurfer/CodeSonar | C/C++ |
C |
CodeSurfer - Sophisticated code
browser that includes pointer analysis, call graphs, dependency chains,
etc. CodeSonar - Analysis for null dereferences, div by zero, buffer over/underruns, memory errors, format string vulnerabilities, etc. |
| Fortify |
C/C++/Java |
C |
Commercial analysis tool focused
on security vulnerabilities like buffer
over/underruns, format string
vulnerabilities, SQL injection attacks, etc.
|
| Agitar |
Java |
C |
Commercial test generation
tool. Also checks "coding rules."
|
| Automated
Test Designer |
Java? |
C |
Automated test generation from
requirements |
| Airac5 |
C |
R |
Static Analyzer for Automatic Detection of Buffer Overrun Errors in C Programs |
| Intel
VTune performance analyzer |
Windows/Linux |
C |
Profiling/performance
analysis. Educational license available from instructor. |
| Lackwit |
C |
R |
Alias analysis for program
understanding. |
| Predictable Assembly
from Certifiable Code (PACC) |
CCL architecture description
language |
R |
Architectural behavior and
performance analysis |