Lincheck is a practical and user-friendly model-checking framework for testing concurrent algorithms on the JVM. Its general API allows testing any concurrent code, while the data structures API takes a list of operations, auto-generates random concurrent scenarios, studies them with the model checker, and verifies each outcome for linearizability.

The framework was introduced at CAV ’23, is maintained on GitHub, and features in recent KotlinConf and Hydra (1, 2) talks.

The workshop drills into both APIs. Participants will: (1) learn Lincheck’s fundamentals and develop an intuition for the Lincheck internals; (2) write tests for generic concurrent code; (3) use the data‑structure API to verify queues, hash tables, and similar structures under constraints such as single‑writer and checking for lock‑freedom; and (4) reproduce and analyze a real race condition in the Java standard library. All tasks run locally on attendees’ laptops. By the end, participants will be equipped to integrate Lincheck into their own projects to systematically validate concurrent behavior.