Popescu, A.; Hölzl, J.; Nipkow, T. Formal Verification of Language-Based Concurrent Noninterference. JFR 2013, 6, 1-30.