(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic

Vlad Rusu, David Nowak

Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems…