swMATH ID: 13773
Software Authors: Herdt, Vladimir; Le, Hoang M.; Große, Daniel; Drechsler, Rolf
Description: Lazy-CSeq-SP: boosting sequentialization-based verification of multi-threaded C programs via symbolic pruning of redundant schedules. 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.
Homepage: http://link.springer.com/chapter/10.1007%2F978-3-319-24953-7_18
Keywords: formal verification; concurrency; sequentialization
Related Software: CBMC; Cseq; MU-CSeq; AProVE; CEGAR; Ultimate Kojak; Symbiotic 2; CPAlien; Jakstab; FrankenBit; ASTREE; SatAbs; Orion; Threader; CPAchecker; Predator; Oz; SLAM; BLAST; GitHub
Cited in: 4 Documents

Cited in 0 Serials

Citations by Year