Reductions for Safety Proofs (Extended Version)

TL;DR

This paper introduces a general framework for simplifying proofs of concurrent programs through context-aware reductions, enhancing automated verification capabilities for complex programs.

Contribution

It presents a novel concept of context in program reductions and demonstrates their effectiveness in automating proofs for complex concurrent programs.

Findings

Effective reduction techniques for concurrent program verification

Introduction of context-based reductions for proof simplification

Enhanced automation in correctness proofs for complex programs

Abstract

Program reductions are used widely to simplify reasoning about the correctness of concurrent and distributed programs. 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. The most novel contribution of this paper is the introduction of the concept of context in the definition of program reductions. We demonstrate how commutativity of program steps in some program contexts can be used to define a generic class of sound reductions which can be used to automatically produce proofs for programs whose complete Floyd-Hoare style proofs are theoretically beyond the reach of automated verification technology of today.