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

pldi-2019-papers
10:00 - 11:00: PLDI Research Papers - Verification II at 229AB
Chair(s): Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia
pldi-2019-papers10:00 - 10:20
Talk
Parosh Aziz AbdullaUppsala University, Sweden, Jatin AroraIIT Bombay, India, Mohamed Faouzi AtigUppsala University, Shankaranarayanan KrishnaIIT Bombay, India
pldi-2019-papers10:20 - 10:40
Talk
Sandeep DasguptaUniversity of Illinois at Urbana-Champaign, USA, Daejun ParkUniversity of Illinois at Urbana-Champaign, Theodoros KasampalisUniversity of Illinois at Urbana-Champaign, USA, Vikram AdveUniversity of Illinois at Urbana-Champaign, Grigore RosuUniversity of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached
pldi-2019-papers10:40 - 11:00
Talk
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