-
Notifications
You must be signed in to change notification settings - Fork 6
Home
This is not directly related to eclipse. Just putting it down here to avoid creating a new project/wiki.
⭐ ⭐ ⭐ means : Recently updated, well documented, liberal license, etc.
(base on which analysers are built)
A framework for building model checkers, and some readily available checkers.
Bug picker ⭐ ⭐ ⭐
BugPicker analyzes the control- and data-flow of applications to identify code issues that affect overall quality of the software.
IteRace ⭐ ⭐ ⭐
IteRace is a static race detection tool, described in this paper.
Seems better than JChord, with far fewer false positives. See comparison in the paper.
Hopper ⭐ ⭐ ⭐
Chord ⭐ ⭐
Tends to output many false positives (several tens of thousands, where IteRace only emits one or two) On the plus side, it is a framework to write custom analyses, and has an active discussion group
JOANA ⭐ ⭐ ⭐
JOANA analyses Java programs for security leaks (Information Flow Control, IFC). It guarantees to find all violations of integrity or confidentiality – that is, all leaks which result from illegal information flow within a program.
KeshMesh ⭐ ⭐
Good but is not actively maintained right now.
Infeasible code detection.
Inconsistent code detection.
(not much info available)
This was the tool used to find a bug in TimSort in Java and Python.
Data centric concurrency control. Requires modifying the Java source that needs to be then translated to pure Java.
Can't find an executable. Perhaps not public domain. An automatic inference of required AJ annotations is available with this tool.
The Java Concolic Unit Testing Engine (jCUTE) automatically generates unit tests for Java programs. jCUTE is able to generate test cases that execute many different execution paths in real Java programs.
Not public domain, but free for non-commerical use.
Open source concolic testing tool.
It narrates some historical background about extended type checking in Java.
Collection of various verification tools, formal languages etc.