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

Stateless Model Checking (SMC) is a verification technique for concurrent programs that checks for safety violations by exploring all possible thread interleavings. SMC is usually coupled with Partial Order Reduction (POR), which exploits the independence of instructions to avoid redundant explorations when an equivalent one has already been considered. While effective POR techniques have been developed for many different memory models, they are only able to exploit independence at the \emph{instruction level}, which makes them unsuitable for programs with coarse-grained synchronization mechanisms such as \emph{locks}.

We present a lock-aware POR algorithm, \emph{LAPOR}, that exploits independence at both \emph{instruction} and \emph{critical section levels}. This enables LAPOR to explore exponentially fewer interleavings than the state-of-the-art techniques for programs that use locks conservatively. Our algorithm is sound, complete, and optimal, and can be used for verifying programs under several different memory models. We implement LAPOR in a tool and show that it can be exponentially faster than the state-of-the-art model checkers.

Fri 25 Oct

splash-2019-oopsla
14:00 - 15:30: OOPSLA - Model Checking at Templars
Chair(s): Casper Bach PoulsenDelft University of Technology
splash-2019-oopsla14:00 - 14:22
Talk
Krishnendu ChatterjeeIST Austria, Andreas PavlogiannisEPFL, Viktor TomanIST Austria (Institute of Science and Technology Austria)
DOI
splash-2019-oopsla14:22 - 14:45
Talk
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
Talk
Igor KonnovInria Nancy - Grand Est, France, Jure KukovecTU Wien, Austria, Thanh-Hai TranTU Wien, Austria
DOI
splash-2019-oopsla15:07 - 15:30
Talk
Michalis KokologiannakisMPI-SWS, Germany, Azalea RaadMPI-SWS, Germany, Viktor VafeiadisMPI-SWS, Germany
DOI