G. Schellhorn, M. Wedel, O. Travkin, J. König, and H. Wehrheim, “FastLane Is Opaque – a Case Study in Mechanized Proofs of Opacity,” in Software Engineering and Formal Methods, Cham: Springer International Publishing, 2018, pp. 105–120.