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