FastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity. - Gerhard Schellhorn; Monika Wedel; Oleg Travkin; Jürgen König; Heike Wehrheim (SEFM, 2018)