Wed 20 Jun 2018 14:25 - 14:50 at Grand Ballroom AB - Concurrency and Termination Chair(s): Iulian Neamtiu

A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is undecidable. A technique proposed by Qadeer and Rehof, to bound the number of context switches allowed between the threads, leads to an incomplete solution that is, however, believed to catch ``most bugs'' in practice. The question whether the technique can also prove the absence of bugs at least in some cases has remained largely open.

In this paper we introduce a broad verification methodology for resource-parameterized programs that observes how changes to the resource parameter affect the behavior of the program. Applied to the context-unbounded analysis problem (CUBA), the methodology results in partial verification techniques for procedural concurrent programs. Our solutions may not terminate, but are able to both refute and prove context-unbounded safety for concurrent recursive threads. We demonstrate the effectiveness of our method using a variety of examples, the safe of which cannot be proved safe by earlier, context-bounded methods.

Wed 20 Jun

pldi-2018-papers
14:00 - 15:40: PLDI Research Papers - Concurrency and Termination at Grand Ballroom AB
Chair(s): Iulian NeamtiuNew Jersey Institute of Technology
pldi-2018-papers14:00 - 14:25
Talk
Lucas BrutschyETH Zurich, Dimitar DimitrovETH Zurich, Switzerland, Peter MüllerETH Zurich, Martin VechevETH Zürich
pldi-2018-papers14:25 - 14:50
Talk
Peizun LiuNortheastern University, USA, Thomas WahlNortheastern University
Media Attached
pldi-2018-papers14:50 - 15:15
Talk
Kostas FerlesUT Austin, Jacob Van GeffenUT Austin, Isil DilligUT Austin, Yannis SmaragdakisUniversity of Athens
Media Attached
pldi-2018-papers15:15 - 15:40
Talk
Yu-Fang Chen, Matthias HeizmannUniversity of Freiburg, Germany, Ondrej LengalBrno University of Technology , Yong LiInstitute of Software, Chinese Academy of Sciences, Ming-Hsien TsaiAcademia Sinica, Taiwan, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences
Media Attached