Andreas Katis, Andrew Gacek, Michael W. Whalen: Machine-Checked Proofs for Realizability Checking Algorithms. VSTTE 2015: 110-123