Authors: Vladimir Herdt, Universität Bremen, DE; Hoang Minh Le, Universität Bremen, DE; Daniel Große, Universität Bremen, DE; Rolf Drechsler, Universität Bremen, DE
Zusammenfassung:
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.
Publication Date: 2015/10/12
Location of Publication: International Symposium on Automated Technology for Verification and Analysis (ATVA), Shanghai, China
Keyword: Verification
