A Program Logic For Dependence Analysis
INTEGRATED FORMAL METHODS, IFM 2019(2019)
摘要
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.
更多查看译文
关键词
Data dependence, Program verification, Static analysis
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络