AbPress: Flexing Partial-Order Reduction and Abstraction

TL;DR

AbPress is a novel model checking algorithm that combines partial-order reduction and lazy abstraction to efficiently verify multi-threaded programs by summarizing shared variable accesses.

Contribution

It introduces AbPress, a new algorithm that fuses source-set based partial-order reduction with lazy abstraction, enhancing efficiency in concurrent program analysis.

Findings

AbPress outperforms existing tools in benchmarks.

The summarization of shared variable accesses improves reduction effectiveness.

Implementation in Impara demonstrates practical applicability.

Abstract

Partial-order reduction (POR) and lazy abstraction with interpolants are two complementary techniques that have been successfully employed to make model checking tools for concurrent programs effective. In this work, we present AbPress - Abstraction-based Partial-order Reduction with Source-Sets - an algorithm that fuses a recently proposed and powerful dynamic POR technique based on source-sets and lazy abstraction to obtain an efficient software model checker for multi-threaded programs. It trims the inter- leaving space by taking the abstraction and source-sets into account. We amplify the effectiveness of AbPress with a novel solution that summarizes the accesses to shared variables over a collection of interleavings. We have implemented AbPress in a tool that analyzes concurrent programs using lazy abstraction, viz., Impara. Our evaluation on the effectiveness of the presented approach has been encouraging. AbPress compares favorably to existing state-of-the-art tools in the landscape.