PV2 Violatgenerates classes attempting to violate properties

Tool to generate tests that witness violations to atomicity or weaker consistency properties in concurrent objects.

Application domain/field

Type of tool

Test generator

Expected input



Name of a single Java class that is available on the classpath or in a user-provided JAR

Expected output

Reports test results, signalling any discovered consistency violations.


In principle Violat outputs a sequence of Java classes which can be tested with off-the-shelf back-end analysis engines. It integrates with JPF and Java Concurrency Stress, thus it is able to provide results directly.


License: MIT


Repository: https://github.com/michael-emmi/violat

Related papers

Last publication date

12 July 2019

Related tools

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.