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.
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
- Yeolekar, Anand; Madhukar, Kumar; Bhutada, Dipali; Venkatesh, R.: Sequentialization using timestamps (2017)
- Travkin, Oleg; Wehrheim, Heike: Verification of concurrent programs on weak memory models (2016)
- Herdt, Vladimir; Le, Hoang M.; Große, Daniel; Drechsler, Rolf: Lazy-CSeq-SP: boosting sequentialization-based verification of multi-threaded C programs via symbolic pruning of redundant schedules (2015)
- Inverso, Omar; Tomasco, Ermenegildo; Fischer, Bernd; La Torre, Salvatore; Parlato, Gennaro: Lazy-cseq: A lazy sequentialization tool for C. (Competition contribution) (2014) ioport