VeriFIT Repository of Test Cases for Concurrency Testing

Repository description

This repository contains test cases which our group VeriFIT uses in papers targeting concurrency testing in Java. Each test case contains all data needed for its compilation (i.e. source code, script demonstrating its build process in common environment) and short documentation describing the program.

Available test cases

The programs are provided as they are with no warranty. Please inform us by sending an email if you like them and use them in your work. We appreciate any comments or suggestions as well.
Name Language Size Error type
Airlines Java 0.3 kLOC, 8 classes Atomicity violation
Animator Java 1.5 kLOC, 31 classes Data race, Atomicity violation
Bank Java 0.1 kLOC, 2 classes Data race, Atomicity violation
Cache4j Java 1.7 kLOC, 66 classes No known error
Crawler Java 1.2 kLOC, 19 classes Atomicity violation
Dining philosophers Java 0.1 kLOC, 6 classes Deadlock
Elevator Java 1.2 kLOC, 12 classes Data race, atomicity violation
FTPServer Java 12.2 kLOC, 120 classes Data race, atomicity violation
HEDC Java 12.7 kLOC, 747 classes No known error
Moldyn Java 0.8 kLOC, 14 classes No known error
Montecarlo Java 1.4 kLOC, 22 classes No known error
Raytracer Java 1.0 kLOC, 22 classes No known error
Rover Java 5.4 kLOC, 82 classes Atomicity violation, deadlock
Sor Java 7.2 kLOC, 256 classes No known error
Tsp Java 0.4 kLOC, 8 classes No known error
TIDOrbJ Java 84.3 kLOC, 1399 classes Atomicity violation

Links to similar repositories and/or benchmarks

If you know an interesting site with benchmarks and/or programs containing concurrency and are not yet listed here, please let us know. This page focus on software testing and therefore only benchmarks with this purpose are listed (i.e., e.g., SAT competition benchmark is not listed here).
Database of big real-life projects with a list of uniformly described bug reports classified as real errors or false positives. The database contains 1150 bug-reports of 11 error types produced by several bug-detection tools run on the Linux 2.6.28 kernel. The database also contains bug reports for examples from Competition on Software Verification (listed bellow).
Software-artifact Infrastructure Repository
The repository contains many Java and C, C++, and C# software systems, in multiple versions, together with supporting artifacts such as test suites, fault data, and scripts. The repository also includes documentation on how to use these objects in experimentation, supporting tools that facilitate experimentation, and information on the processes used to select, organize, and enhance the artifacts, and supporting tools that help with these processes.
Qualitas Corpus
The Qualitas Corpus is a curated collection of software systems intended to be used for empirical studies of code artefacts. The primary goal is to provide a resource that supports reproducible studies of software. The current release of the Corpus contains open-source Java software systems, often multiple versions.
Database of Java programs curated by IBM HRL
Database of 40 small programs (most of them have less than 300 LoC) written in Java and containing well documented concurrency error such as atomicity violations, deadlocks, orphaned thread, etc. The database is not publicly available. Please contact Rachel Brill from IBM HRL to get access.
Competition on Software Verification (SV-COMP) benchmarks
A database of 7000 small programs of various size containing various classes of errors (including concurrency). The database also contain programs that are very hard to verify. 2868 of them are used for the competition, rest is maintained for demonstration purposes. Most of the programs are in C and preprocessed by CIL.
SF100 Benchmark
Randomly selected 100 Java projects from SourceForge. The benchmark is not only very large but more importantly it is statistically sound and representative for open source Java projects.
Dacapo Benchmark
A benchmark suite which is intended as a tool for Java benchmarking by the programming language, memory management and computer architecture communities. It consists of a set of open source, real world applications with non-trivial memory loads.
NECLA Verification Benchmarks
A set of 15 C/C++ programs with various C/C++ specific bugs including real programs and various bug pattern sources.
CPROVER Benchmarking Toolkit
A set of 8 C/C++ real programs (including Linux 2.6.19 kernel) and patches which makes them verifiable by model checking tool.
VerifyThis is a collection of problems (and solutions) in formal verification of object-oriented software. The benchmark contains 43 problems and solutions.
Challenge Benchmarks for Verification of Real-time Programs
Set of 6 Java and C programs with real problems including 1 concurrency problem.


This work was supported by the Czech Ministry of Education (project Kontakt II LH13265) and the EU/Czech Interdisciplinary Excellence Research Teams Establishment project (CZ.1.07/2.3.00/30.0005).