Analysis Tool List

For all commercial tools listed, either there is a free trial version or academic version available, or we have a CMU license for this class.  For the tools that have been evaluated in the past, a link to the students report is given.

Tool Name
Platform
Commercial/
Research
Comments
Coverity
C, C++
C
Commercial analysis tool that can find null dereferences, buffer over/underruns, memory and concurrency errors, format string vulnerabilities, etc. Tool license available through the instructor. Report 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.
Tool license available through the instructor.
Klocwork
C/C++/Java
C
Commercial analysis tool that can find null dereferences, buffer over/underruns, memory errors, format string vulnerabilities, etc. Tool license for the enterprise edition is available through the instructor.  Tool license available through the instructor.
Fortify
C/C++/Java
C
Commercial analysis tool focused on security vulnerabilities like buffer over/underruns, format string vulnerabilities, SQL injection attacks, etc. Tool license for the enterprise edition is available through the instructor.
Agitar
Java
C
Commercial test generation tool.  Also checks "coding rules."  Tool license available through the instructor.
Parasoft
C/C++/Java/.NET
C
Commercial test generation tool.  Also checks "coding rules."
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
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.

Past Implementation projects
Past Literature Surveys
Other analysis tools to check out: