Model checking is one of the most effective tools for verifying high-criticality programs, such as those used in security applications, automobiles, and medical devices. However, model checking can be computationally expensive, as it requires analyzing a large number of system states, so efficient algorithms and specialized tools are needed for the verification of large-scale systems. The goal of this project is to design, develop, and implement a new verification system for lock-free data structures for concurrent C programs. This system will be complemented by a BMC-based concurrent program analysis tool called Lazy-CSeq which has a more famous and robust tool called CBMC as its analysis backend. The search was conducted on the GitHub platform using Lock-Free Queue (LFQ) and Data Structures (Data Structures) as keywords. At the end of the analysis, the generated trace was found to be valid, indicating that the analyzed data structure does indeed contain a bug.
For more details take a look at the report