Java Goes TLA+. - Hannes Lau; Uwe Nestmann (TASE, 2011)