Write a Blog >>
Wed 22 Jan 2020 15:56 - 16:18 at Ile de France III (IDF III) - Concurrency / Memory Chair(s): Susmit Sarkar

Program reductions are used widely to simplify reasoning about the correctness of concurrent and distributed programs. Different reduction techniques are often tailored towards specific classes of programs, for example message passing vs shared memory. In this paper, we propose a general approach to proof simplification of concurrent programs based on exploring generic classes of reductions. We introduce two classes of sound program reductions, study their theoretical properties, show how they can be effectively used in algorithmic verification, and demonstrate that they are very effective in producing proofs of a diverse class of programs without targeting specific syntactic properties of these programs. We modify the classic counterexample-guided refinement loop of automated program verification so that, in addition to proof search, it also searches for a program reduction that admits a substantially simpler proof of correctness compared to the original program. This methodology, hence, succeeds in automatically generating proofs for programs whose full proofs are theoretically outside the reach of current automated verification technology.

Wed 22 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

15:35 - 16:40: Research Papers - Concurrency / Memory at Ile de France III (IDF III)
Chair(s): Susmit SarkarUniversity of St. Andrews
POPL-2020-Research-Papers15:35 - 15:56
Azalea RaadMPI-SWS, Germany, John WickersonImperial College London, Gil NeigerIntel Corporation, Viktor VafeiadisMPI-SWS, Germany
Link to publication DOI Media Attached
POPL-2020-Research-Papers15:56 - 16:18
Azadeh FarzanUniversity of Toronto, Anthony VandikasUniversity of Toronto
Link to publication DOI Media Attached
POPL-2020-Research-Papers16:18 - 16:40
Hoang-Hai DangMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Jan-Oliver KaiserMPI-SWS, Derek DreyerMPI-SWS
Link to publication DOI Media Attached