A pragmatic approach to stateful partial order reduction

Cirisci, Berk and Enea, Constantin and Farzan, Azadeh and Mutluergil, Süha Orhun (2023) A pragmatic approach to stateful partial order reduction. In: 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023, Boston, MA, USA

Full text not available from this repository. (Request a copy)

Abstract

Partial order reduction (POR) is a classic technique for dealing with the state explosion problem in model checking of concurrent programs. Theoretical optimality, i.e., avoiding enumerating equivalent interleavings, does not necessarily guarantee optimal overall performance of the model checking algorithm. The computational overhead required to guarantee optimality may by far cancel out any benefits that an algorithm may have from exploring a smaller state space of interleavings. With a focus on overall performance, we propose new algorithms for stateful POR based on the recently proposed source sets, which are less precise but more efficient than the state of the art in practice. We evaluate efficiency using an implementation that extends Java Pathfinder in the context of verifying concurrent data structures.
Item Type: Papers in Conference Proceedings
Divisions: Faculty of Engineering and Natural Sciences
Depositing User: Süha Orhun Mutluergil
Date Deposited: 07 May 2023 19:25
Last Modified: 07 May 2023 19:25
URI: https://research.sabanciuniv.edu/id/eprint/45488

Actions (login required)

View Item
View Item