A Program Logic for Dependence Analysis.

Read and write dependences of program variables are essential to determine whether and how a loop or a whole program can be parallelized. State-of-the-art tools for parallelization use approaches that over- as well as under-approximate to compute dependences and they lack a formal foundation. In this paper, we give formal semantics of read and write data dependences and present a program logic that is able to reason about dependences soundly and with full precision. The approach has been implemented in the deductive verification tool KeY for the target language Java.