We are looking forward to a presentation by Marieke Huisman.
Time and Date: 8 October 2025, 16:00 CEST,
As a follow-up to the March 2024 Lorentz Center workshop on Contract Languages, we will host a series of online presentations and discussions around formal methods with contract languages, aligning with the LTC goal of enabling information exchange between different formal systems.
Contracts for Concurrent Software with VerCors
Ensuring correctness in concurrent and distributed software is notoriously challenging due to shared memory access, synchronization, and potential data races. This talk introduces the language concepts of VerCors, a powerful verification toolset designed to reason about concurrent Java programs using permission-based contracts. We will explore key concepts such as permission annotations, fork-join concurrency, parallel blocks, locks, and atomics—each illustrated with practical examples and verification strategies.
The interactive tutorial will guide participants through hands-on exercises, including verifying concurrent algorithms like parallel sum and sparse matrix multiplication. Attendees will learn how to specify and verify functional behavior and synchronization properties using VerCors, gaining insights into how formal methods can enhance software reliability in multi-threaded environments.
If you want to reiterate over the challenges and solutions:
If you are interested in joining, drop a mail to Mattias Ulbrich for the link.