Lazy-CSeq-SP: Boosting sequentialization-based verification of multi-threaded c programs via symbolic pruning of redundant schedules

Abstract

Sequentialization has been shown to be an effective symbolic verification technique for concurrent C programs using POSIX threads. Lazy-CSeq, a tool that applies a lazy sequentialization scheme, has won the Concurrency division of the last two editions of the Competition on Software Verification. The tool encodes all thread schedules up to a given bound into a single non-deterministic sequential C program and then invokes a C model checker. This paper presents a novel optimized implementation of lazy sequentialization, which integrates symbolic pruning of redundant schedules into the encoding. Experimental evaluation shows that our tool outperforms Lazy-CSeq significantly on many benchmarks.