A JMM-faithful non-interference calculus for Java

Abstract. We present a calculus for establishing non-interference of several Java threads running in parallel. The proof system is built atop an implemented sequential Java Dynamic Logic calculus with 100 % Java Card coverage. We present two semantic and one syntactic type of noninterference conditions to make reasoning efficient. In contrast to previous works in this direction, our method takes into full account the weak guarantees of the Java Memory Model concerning visibility and ordering of memory updates between threads.