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

Displayed time zone: (UTC) Coordinated Universal Time change

08:05 - 09:05
I22-TestingTechnical Papers / Demonstrations at Baekje
Chair(s): Phil McMinn University of Sheffield
08:05
3m
Talk
FuRong: Fusing Report of Automated Android Testing on Multi-DevicesDemo
Demonstrations
Yuanhan Tian Nanjing University, Shengcheng Yu Nanjing University, China, Chunrong Fang Nanjing University, Peiyuan Li Nanjing University
08:08
12m
Talk
MemLock: Memory Usage Guided FuzzingArtifact ReusableTechnicalArtifact Available
Technical Papers
Cheng Wen Shenzhen University, Haijun Wang Ant Financial Services Group, China; CSSE, Shenzhen University, China, Yuekang Li Nanyang Technological University, Shengchao Qin University of Teesside, Yang Liu Nanyang Technological University, Singapore, Zhiwu Xu Shenzhen University, Hongxu Chen Research Associate, Xiaofei Xie Nanyang Technological University, Geguang Pu East China Normal University, Ting Liu Xi'an Jiaotong University
DOI Pre-print Media Attached
08:20
12m
Talk
Symbolic Verification of Message Passing Interface ProgramsArtifact ReusableTechnicalArtifact Available
Technical Papers
Hengbiao Yu National University of Defense Technology, Zhenbang Chen College of Computer, National University of Defense Technology, Changsha, PR China, Xianjin Fu National University of Defense Technology, Ji Wang School of Computer, National University of Defense Technology, China, Zhendong Su ETH Zurich, Switzerland, Jun Sun Singapore Management University, Chun Huang National University of Defense Technology, Wei Dong School of Computer, National University of Defense Technology, China
Pre-print
08:32
12m
Talk
SAVER: Scalable, Precise, and Safe Memory-Error RepairArtifact ReusableTechnicalArtifact Available
Technical Papers
Seongjoon Hong Korea University, Junhee Lee Korea University, South Korea, Jeongsoo Lee Korea University, Hakjoo Oh Korea University, South Korea
08:44
12m
Talk
A Large-Scale Empirical Study on Vulnerability Distribution within Projects and the Lessons LearnedTechnical
Technical Papers
Bingchang Liu Key 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 Meng Institute of Information Engineering, Chinese Academy of Sciences, Chao Zhang Institute for Network Sciences and Cyberspace of Tsinghua University, Feng Li Key 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 Gong Key Laboratory of Network Assessment Technology, Institute of Information Engineering, Chinese Academy of Sciences, China, Min Lin Institute for Network Sciences and Cyberspace of Tsinghua University, Dandan Sun Key Laboratory of Network Assessment Technology, Institute of Information Engineering, Chinese Academy of Sciences, China, Wei Huo Institute of Information Engineering, Chinese Academy of Sciences, Wei Zou Key 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
08:56
3m
Talk
MPI-SV: A Symbolic Verifier for MPI ProgramsDemo
Demonstrations
Zhenbang Chen College of Computer, National University of Defense Technology, Changsha, PR China, Hengbiao Yu National University of Defense Technology, Xianjin Fu National University of Defense Technology, Ji Wang School of Computer, National University of Defense Technology, China
Pre-print