Iekkë: A Bounded-Round Partial-Order Encoding Verification Tool for Concurrent C Programs
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...