N. E. Flick, “Proving Correctness of Graph Programs Relative to Recursively Nested Conditions”, ECEASST, vol. 73, Apr. 2016.