Iekkë: A Bounded-Round Partial-Order Encoding Verification Tool for Concurrent C Programs

Abstract

We present Iekkë, a BMC tool for verifying multi-threaded C programs. It implements a new bounded-round partial-order encoding for the sequential consistency shared-memory model. The encoding combines the compactness of lazy sequentialization with the structural precision of the partial-order approach. Its concurrency constraints grow linearly in the number of shared-memory events and in the round bound 𝑘—avoiding the quadratic/cubic blow-up of classical partial-order encodings—and are fully propositional, enabling the use of an off-the-shelf SAT solver. Iekkë is built on top of the CBMC/Deagle infrastructure and replaces only the concurrency constraint module. It supports concurrent reachability checking, data race detection, and the usual safety property checks implemented by CBMC. Iekkë won the Bronze medal in the Concurrency category of SV-COMP 2026.