Iekkë: A SAT-Based Bounded-Round Verifier for Multi-Threaded Programs (Competition Contribution)

Abstract Iekkë is a sequentialization-inspired bounded model checking (BMC) tool for verifying multi-threaded C programs. It is derived from Deagle and reuses the CBMC front-end for parsing, goto-program construction, loop unwinding, and SSA-based formula generation. Iekkë differs from both CBMC and Deagle in its treatment of shared-memory interactions: it replaces the classic partial-order memory constraints with a bounded-round encoding inspired by lazy sequentialization. The resulting shared-memory constraints are linear in the number of memory events of the bounded program and linear in the round bound  k , avoiding the quadratic/cubic growth typical of partial-order encodings. Because the concurrency constraints are compact and purely propositional, Iekkë relies on an off-the-shelf SAT solver (e.g., MiniSAT ) rather than a dedicated ordering-theory solver. Iekkë supports reachability, assertion and data-race checking, and produces SV-COMP witnesses for violations.