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
|15:35 - 15:56|
Azalea RaadMPI-SWS, Germany, John WickersonImperial College London, Gil NeigerIntel Corporation, Viktor VafeiadisMPI-SWS, GermanyLink to publication DOI Media Attached
|15:56 - 16:18|
|Link to publication DOI Media Attached|
|16:18 - 16:40|
Hoang-Hai DangMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Jan-Oliver KaiserMPI-SWS, Derek DreyerMPI-SWSLink to publication DOI Media Attached