Tue 17 Jan 2023 16:00 - 16:15 at Arlington - Model Checking Chair(s): Eric Koskinen

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.

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:00 - 17:30
Model CheckingVMCAI at Arlington
Chair(s): Eric Koskinen Stevens Institute of Technology
16:00
15m
Talk
A Pragmatic Approach to Stateful Partial Order ReductionRecorded
VMCAI
Berk Cirisci IRIF, University Paris Diderot and CNRS, France, Constantin Enea Ecole Polytechnique / LIX / CNRS, Azadeh Farzan University of Toronto, Suha Orhun Mutluergil Sabanci University, Turkey
16:15
15m
Talk
StaticPersist : Compiler Support for PMEM ProgrammingRecorded
VMCAI
Sorav Bansal IIT Delhi and CompilerAI Labs
16:30
30m
Talk
Compositional Verification of Stigmergic Collective Systems
VMCAI
Luca Di Stefano University of Gothenburg, Sweden, Frederic Lang
17:00
30m
Talk
Synthesizing History and Prophecy Variables for Symbolic Model Checking
VMCAI
Cole Vick , Kenneth L. McMillan University of Texas at Austin