Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy

Eden Frenkel, Kenneth L. McMillan, Oded Padon +1

We propose an incremental approach for safety proofs that decomposes a proof with a complex inductive invariant into a sequence of simpler proof steps. Our proof system combines ru…