Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Fri 25 Oct 2019 14:00 - 14:22 at Templars - Model Checking Chair(s): Casper Bach Poulsen

The verification of concurrent programs remains an open challenge,
as thread interaction has to be accounted for, which leads to state-space explosion.
Stateless model checking battles this problem by exploring traces rather than states of the program.
As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques
are used to partition the trace space into equivalence classes, and explore a few representatives from each class.
The standard equivalence that underlies most DPOR techniques is the \emph{happens-before} equivalence,
however recent works have spawned a vivid interest towards coarser equivalences.
The efficiency of such approaches is a product of two parameters:
(i)~the size of the partitioning induced by the equivalence, and
(ii)~the time spent by the exploration algorithm in each class of the partitioning.

In this work, we present a new equivalence, called \emph{value-happens-before} and show that it has two appealing features.
First, value-happens-before is always at least \emph{as coarse as} the happens-before equivalence, and can be even exponentially coarser.
Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded.
We present an algorithm called \emph{value-centric} DPOR ($\mathsf{VCDPOR}$), which explores the underlying partitioning using polynomial time per class.
Finally, we perform an experimental evaluation of $\mathsf{VCDPOR}$ on various benchmarks, and compare it against other state-of-the-art approaches.
Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning,
which leads to a considerable reduction in the running time for exploring the whole partitioning.

Fri 25 Oct

Displayed time zone: Beirut change

14:00 - 15:30
Model CheckingOOPSLA at Templars
Chair(s): Casper Bach Poulsen Delft University of Technology
14:00
22m
Talk
Value-Centric Dynamic Partial Order Reduction
OOPSLA
Krishnendu Chatterjee IST Austria, Andreas Pavlogiannis EPFL, Viktor Toman IST Austria (Institute of Science and Technology Austria)
DOI
14:22
22m
Talk
Optimal Stateless Model Checking for Reads-From Equivalence under Sequential Consistency
OOPSLA
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Bengt Jonsson Uppsala University, Sweden, Magnus Lång Uppsala University, Sweden, Tuan Phong Ngo Uppsala University, Sweden, Konstantinos (Kostis) Sagonas Uppsala University, Sweden
DOI Pre-print
14:45
22m
Talk
TLA+ Model Checking Made Symbolic
OOPSLA
Igor Konnov Inria Nancy - Grand Est, France, Jure Kukovec TU Wien, Austria, Thanh-Hai Tran TU Wien, Austria
DOI
15:07
22m
Talk
Effective Lock Handling in Stateless Model Checking
OOPSLA
Michalis Kokologiannakis MPI-SWS, Germany, Azalea Raad MPI-SWS, Germany, Viktor Vafeiadis MPI-SWS, Germany
DOI