Write a Blog >>
ICSE 2020
Wed 24 June - Thu 16 July 2020
Fri 10 Jul 2020 08:20 - 08:32 at Baekje - I22-Testing Chair(s): Phil McMinn

Message passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). In this work, we present MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for automatically verifying MPI programs with non-blocking operations. MPI-SV combines symbolic execution and model checking in a synergistic way to tackle the challenges in MPI program verification. The synergy improves the scalability and enlarges the scope of verifiable properties. We have implemented MPI-SV\footnote{MPI-SV is available \url{https://mpi-sv.github.io}.} and evaluated it with 111 real-world MPI verification tasks. The pure symbolic execution-based technique successfully verifies 61 out of the 111 tasks (55%) within one hour, while in comparison, MPI-SV verifies 100 tasks (90%). On average, compared with pure symbolic execution, MPI-SV achieves 19x speedups on verifying the satisfaction of the critical property and 5x speedups on finding violations.

Fri 10 Jul
Times are displayed in time zone: (UTC) Coordinated Universal Time change

icse-2020-paper-presentations
08:05 - 09:05: Paper Presentations - I22-Testing at Baekje
Chair(s): Phil McMinnUniversity of Sheffield
Demonstrations08:05 - 08:08
Talk
Yuanhan TianNanjing University, Shengcheng YuNanjing University, China, Chunrong FangNanjing University, Peiyuan LiNanjing University
icse-2020-papers08:08 - 08:20
Talk
Cheng WenShenzhen University, Haijun WangAnt Financial Services Group, China; CSSE, Shenzhen University, China, Yuekang LiNanyang Technological University, Shengchao QinUniversity of Teesside, Yang LiuNanyang Technological University, Singapore, Zhiwu XuShenzhen University, Hongxu ChenResearch Associate, Xiaofei XieNanyang Technological University, Geguang PuEast China Normal University, Ting LiuXi'an Jiaotong University
DOI Pre-print Media Attached
icse-2020-papers08:20 - 08:32
Talk
Hengbiao YuNational University of Defense Technology, Zhenbang ChenCollege of Computer, National University of Defense Technology, Changsha, PR China, Xianjin FuNational University of Defense Technology, Ji WangSchool of Computer, National University of Defense Technology, China, Zhendong SuETH Zurich, Switzerland, Jun SunSingapore Management University, Chun HuangNational University of Defense Technology, Wei DongSchool of Computer, National University of Defense Technology, China
Pre-print
icse-2020-papers08:32 - 08:44
Talk
Seongjoon HongKorea University, Junhee LeeKorea University, South Korea, Jeongsoo LeeKorea University, Hakjoo OhKorea University, South Korea
icse-2020-papers08:44 - 08:56
Talk
Bingchang LiuKey Laboratory of Network Assessment Technology, Institute of Information Engineering, Chinese Academy of Sciences, China; School of CyberSpace Security at University of Chinese Academy of Sciences, China, Guozhu MengInstitute of Information Engineering, Chinese Academy of Sciences, Chao ZhangInstitute for Network Sciences and Cyberspace of Tsinghua University, Feng LiKey Laboratory of Network Assessment Technology, Institute of Information Engineering, Chinese Academy of Sciences, China; School of CyberSpace Security at University of Chinese Academy of Sciences, China, Qi GongKey Laboratory of Network Assessment Technology, Institute of Information Engineering, Chinese Academy of Sciences, China, Min LinInstitute for Network Sciences and Cyberspace of Tsinghua University, Dandan SunKey Laboratory of Network Assessment Technology, Institute of Information Engineering, Chinese Academy of Sciences, China, Wei HuoInstitute of Information Engineering, Chinese Academy of Sciences, Wei ZouKey Laboratory of Network Assessment Technology, Institute of Information Engineering, Chinese Academy of Sciences, China; School of CyberSpace Security at University of Chinese Academy of Sciences, China
Demonstrations08:56 - 08:59
Talk
Zhenbang ChenCollege of Computer, National University of Defense Technology, Changsha, PR China, Hengbiao YuNational University of Defense Technology, Xianjin FuNational University of Defense Technology, Ji WangSchool of Computer, National University of Defense Technology, China
Pre-print