Symbolic Execution of MPI Programs

被引：6
|
作者：
Fu, Xianjin [1 ,2 ]
Chen, Zhenbang [2 ]
Yu, Hengbiao [1 ,2 ]
Huang, Chun [2 ]
Dong, Wei [2 ]
Wang, Ji [1 ,2 ]
机构：
[1] Natl Univ Def Technol, State Key Lab High Performance Comp, Changsha, Hunan, Peoples R China
[2] Natl Univ Def Technol, Coll Comp, Changsha, Hunan, Peoples R China
来源：
2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, Vol 2 | 2015年
关键词：
D O I：
10.1109/ICSE.2015.259
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
MPI is widely used in high performance computing. In this extended abstract, we report our current status of analyzing MPI programs. Our method can provide coverage of both input and non-determinism for MPI programs with mixed blocking and non-blocking operations. In addition, to improve the scalability further, a deadlock-oriented guiding method for symbolic execution is proposed. We have implemented our methods, and the preliminary experimental results are promising.
引用
收藏
页码：809 / 810
页数：2
相关论文
共 50 条
  • [21] Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
    Hensel, Jera
    Giesl, Juergen
    Frohn, Florian
    Stroeder, Thomas
    [J]. SOFTWARE ENGINEERING AND FORMAL METHODS: 14TH INTERNATIONAL CONFERENCE, SEFM 2016, 2016, 9763 : 234 - 252
  • [22] Loop Extended Symbolic Execution on List Manipulating Programs
    Li, Renjian
    Wang, Zhaofei
    Dong, Longming
    [J]. MECHANICAL AND ELECTRONICS ENGINEERING III, PTS 1-5, 2012, 130-134 : 3010 - 3014
  • [23] VALIDATION OF CONCURRENT ADA PROGRAMS USING SYMBOLIC EXECUTION
    MORASCA, S
    PEZZE, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 387 : 467 - 486
  • [24] Symbolic Execution Proofs for Higher Order Store Programs
    Bernhard Reus
    Nathaniel Charlton
    Ben Horsfall
    [J]. Journal of Automated Reasoning, 2015, 54 : 199 - 284
  • [25] A Formal Model for Detecting Bugs by Symbolic Execution of Programs
    A. Yu. Gerasimov
    D. O. Kuts
    A. A. Novikov
    [J]. Programming and Computer Software, 2020, 46 : 731 - 736
  • [26] Symbolic Execution Proofs for Higher Order Store Programs
    Reus, Bernhard
    Charlton, Nathaniel
    Horsfall, Ben
    [J]. JOURNAL OF AUTOMATED REASONING, 2015, 54 (03) : 199 - 284
  • [27] USING SYMBOLIC EXECUTION FOR VERIFICATION OF ADA TASKING PROGRAMS
    DILLON, LK
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1990, 12 (04): : 643 - 669
  • [28] Loop-Extended Symbolic Execution on Binary Programs
    Saxena, Prateek
    Poosankam, Pongsin
    McCamant, Stephen
    Song, Dawn
    [J]. ISSTA 2009: INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, 2009, : 225 - 235
  • [29] Hotspot Symbolic Execution of Floating-Point Programs
    Quan, Minghui
    [J]. FSE'16: PROCEEDINGS OF THE 2016 24TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON FOUNDATIONS OF SOFTWARE ENGINEERING, 2016, : 1112 - 1114
  • [30] Protocol Knowledge Combined Directed Symbolic Execution for Binary Programs
    Huang, Hui
    Lu, Yu-Liang
    Zhao, Jun
    Wu, Zhi-Yong
    [J]. 2013 THIRD INTERNATIONAL CONFERENCE ON INSTRUMENTATION & MEASUREMENT, COMPUTER, COMMUNICATION AND CONTROL (IMCCC), 2013, : 120 - 124
12345