Write a Blog >>
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

14:00 - 15:30: OOPSLA - Model Checking at Templars
Chair(s): Casper Bach PoulsenDelft University of Technology
splash-2019-oopsla14:00 - 14:22
Krishnendu ChatterjeeIST Austria, Andreas PavlogiannisEPFL, Viktor TomanIST Austria (Institute of Science and Technology Austria)
splash-2019-oopsla14:22 - 14:45
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Bengt JonssonUppsala University, Sweden, Magnus LångUppsala University, Sweden, Tuan Phong NgoUppsala University, Sweden, Konstantinos (Kostis) SagonasUppsala University, Sweden
DOI Pre-print
splash-2019-oopsla14:45 - 15:07
Igor KonnovInria Nancy - Grand Est, France, Jure KukovecTU Wien, Austria, Thanh-Hai TranTU Wien, Austria
splash-2019-oopsla15:07 - 15:30
Michalis KokologiannakisMPI-SWS, Germany, Azalea RaadMPI-SWS, Germany, Viktor VafeiadisMPI-SWS, Germany