A Pragmatic Approach to Stateful Partial Order ReductionRecorded
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 JanDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 17:30 | |||
16:00 15mTalk | 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 15mTalk | StaticPersist : Compiler Support for PMEM ProgrammingRecorded VMCAI Sorav Bansal IIT Delhi and CompilerAI Labs | ||
16:30 30mTalk | Compositional Verification of Stigmergic Collective Systems VMCAI | ||
17:00 30mTalk | Synthesizing History and Prophecy Variables for Symbolic Model Checking VMCAI |