Reductions for Safety Proof Simplification
Abstract:
Program reductions are used widely to simplify reasoning about the correctness of concurrent and distributed programs. In this talk, I will present a general approach to proof simplification of concurrent/distributed programs based on exploring generic classes of reductions. The main goal of reductions are to find a sound proof within the means automated verification tools when a full classic proof of the full program is strictly out of reach. I will introduce three (incrementally more expressive) classes of sound program reductions, discuss 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.