Wed 26 Jun 2019 10:00 - 10:20 at 229AB - Verification II Chair(s): Michael Norrish

We address the verification of concurrent programs running under the release-acquire (RA) semantics.
We show that the reachability problem is undecidable even in the case where the input program is finite-state.
Given this undecidability, we follow the spirit of the work on context-bounded analysis for detecting bugs in
programs under the classical SC model, and propose an under-approximate reachability analysis for the case of RA. To this end, we propose a novel notion, called view-switching, and provide a code-to-code translation from an input program under RA to a program under SC. This leads to a reduction, in polynomial time, of the bounded view-switching reachability problem under RA to the bounded context-switching problem under SC. We have implemented a prototype tool VBMC and tested it on a set of benchmarks, demonstrating that many bugs in programs can be found using a small number of view switches.

Wed 26 Jun
Times are displayed in time zone: Tijuana, Baja California change

10:00 - 11:00: Verification IIPLDI Research Papers at 229AB
Chair(s): Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia
10:00 - 10:20
Talk
PLDI Research Papers
Parosh Aziz AbdullaUppsala University, Sweden, Jatin AroraIIT Bombay, India, Mohamed Faouzi AtigUppsala University, Shankaranarayanan KrishnaIIT Bombay, India
10:20 - 10:40
Talk
PLDI Research Papers
Sandeep DasguptaUniversity of Illinois at Urbana-Champaign, USA, Daejun ParkUniversity of Illinois at Urbana-Champaign, Theodoros KasampalisUniversity of Illinois at Urbana-Champaign, USA, Vikram S. AdveUniversity of Illinois at Urbana-Champaign, Grigore RosuUniversity of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached
10:40 - 11:00
Talk
PLDI Research Papers
Li ZhouDepartment of Computer Science and Technology, Tsinghua University, Nengkun YuUniversity of Technology Sydney, Australia, Mingsheng YingUniversity of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University.
Media Attached