A Program Logic for Dependence Analysis

被引：4

作者：

Bubel, Richard ^{[1
]}

Haehnle, Reiner ^{[1
]}

Tabar, Asmae Heydari ^{[1
]}

机构：

[1] Tech Univ Darmstadt, Dept Comp Sci, D-64289 Darmstadt, Germany

来源：

INTEGRATED FORMAL METHODS, IFM 2019 | 2019年 / 11918卷

关键词：

Data dependence; Program verification; Static analysis;

D O I：

10.1007/978-3-030-34968-4_5

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：83 / 100

页数：18

共 50 条

[1] Program dependence analysis of concurrent logic programs and its applications
Zhao, JJ
Cheng, JD
Ushijima, K
[J]. 1996 INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED SYSTEMS, PROCEEDINGS, 1996, : 282 - 291
[2] PROGRAM PARTITION AND LOGIC PROGRAM ANALYSIS
HAN, JL
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1995, 21 (12) : 959 - 968
[3] Separation logic and program analysis
O'Hearn, Peter W.
[J]. STATIC ANALYSIS, PROCEEDINGS, 2006, 4134 : 181 - 181
[4] A program dependence model for concurrent logic programs and its applications
Zhao, JJ
Cheng, JD
Ushijima, K
[J]. IEEE INTERNATIONAL CONFERENCE ON SOFTWARE MAINTENANCE, PROCEEDINGS: SYSTEMS AND SOFTWARE EVOLUTION IN THE ERA OF THE INTERNET, 2001, : 672 - 681
[5] Causal program dependence analysis
Lee, Seongmin
Binkley, Dave
Feldt, Robert
Gold, Nicolas
Yoo, Shin
[J]. Science of Computer Programming, 2025, 240
[6] ANALYSIS OF PROGRAM LOGIC TEST STRATEGIES
LIPAEV, VV
POZIN, BA
BLAU, SA
[J]. CYBERNETICS, 1982, 18 (02): : 195 - 200
[7] Program theory evaluation: Logic analysis
Brousselle, Astrid
Champagne, Francois
[J]. EVALUATION AND PROGRAM PLANNING, 2011, 34 (01) : 69 - 78
[8] Differential methods in logic program analysis
de la Banda, MG
Marriott, K
Stuckey, P
Sondergaard, H
[J]. JOURNAL OF LOGIC PROGRAMMING, 1998, 35 (01): : 1 - 37
[9] DEPENDENCE-BASED PROGRAM ANALYSIS
JOHNSON, R
PINGALI, K
[J]. SIGPLAN NOTICES, 1993, 28 (06): : 78 - 89
[10] Scalable and Approximate Program Dependence Analysis
Lee, Seongmin
[J]. 2020 ACM/IEEE 42ND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: COMPANION PROCEEDINGS (ICSE-COMPANION 2020), 2020, : 162 - 165

← 1 2 3 4 5 →