Matthew Finifter, Adrian Mettler, Naveen Sastry, David A. Wagner: Verifiable functional purity in java. CCS 2008: 161-174