Ultimate GemCutter
Ultimate GemCutter is a software model checker for concurrent programs.
In order to verify a concurrent program, all possible interleavings of actions by different threads must be considered. GemCutter combines the abstraction refinement-based verification algorithm trace abstraction with reasoning based on the principle of commutativity, i.e., the observation that some actions of different threads can be reordered without affecting program correctness. Based on commutativity, GemCutter reduces a given program (using partial order reduction algorithms) to a sound subset of interleavings, and verifies the reduced program.
Commutativity-based reduction both speeds up the verification, and allows GemCutter to verify programs that would otherwise require complicated invariants.
Awards
- Ultimate GemCutter won 2nd place in the ConcurrencySafety category at the SV-COMP 2024
- Ultimate GemCutter won 3rd place in the ConcurrencySafety category at the SV-COMP 2023.
- Ultimate GemCutter won 3rd place in the ConcurrencySafety category at the SV-COMP 2022.
GemCutter also won 1st place in the NoDataRace demo category.
Web interface
Ultimate GemCutter is available via a web interface.
Developers
Ultimate GemCutter is maintained by Dominik Klumpp.
Since Ultimate GemCutter is a toolchain of the Ultimate software analysis framework, many people were involved in the development (especially our bachelor and master students). If you are a student at our university and you like to contribute to Ultimate in a project, laboratory, or thesis then contact Dominik Klumpp or any other Ultimate developer.
Download
We try to provide regular releases for Windows and Linux at our GitHub release page.
Related Publications
[1] Azadeh Farzan, Dominik Klumpp, Andreas Podelski: Sound Sequentialization for Concurrent Program Verification. PLDI 2022
[2] Dominik Klumpp, Daniel Dietsch, Matthias Heizmann, Frank Schüssele, Marcel Ebbinghaus, Azadeh Farzan, Andreas Podelski: Ultimate GemCutter and the Axes of Generalization (Competition Contribution). TACAS 2022
[3] Azadeh Farzan, Dominik Klumpp, Andreas Podelski: Stratified Commutativity in Verification Algorithms for Concurrent Programs. POPL 2023