Fri 10 Jul 2020 08:56 - 08:59 at Baekje - I22-Testing Chair(s): Phil McMinn
Fri 10 Jul 2020 09:10 - 10:00 at Live Demo Room - ID6-Live Demos
Fri 10 Jul 2020 09:10 - 10:00 at Live Demo Room - ID6-Live Demos
Message passing is the primary programming paradigm in high-performance computing. However, developing message passing programs is challenging due to the non-determinism caused by parallel execution and complex programming features such as non-deterministic communications and asynchrony. We present MPI-SV, a symbolic verifier for verifying the parallel C programs using message passing interface (MPI). MPI-SV combines symbolic execution and model checking in a synergistic manner to improve the scalability and enlarge the scope of verifiable properties. We have applied MPI-SV to real-world MPI C programs. The experimental results indicate that MPI-SV can, on average, achieve 19x speedups in verifying deadlock-freedom and 5x speedups in finding counter-examples. MPI-SV can be accessed at https://mpi-sv.github.io, and the demonstration video is at https://youtu.be/zzCY0CPDNCw.
Fri 10 JulDisplayed time zone: (UTC) Coordinated Universal Time change
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 3mTalk | 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 12mTalk | MemLock: Memory Usage Guided Fuzzing Technical Papers Cheng Wen Xidian 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 12mTalk | Symbolic Verification of Message Passing Interface Programs 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 12mTalk | SAVER: Scalable, Precise, and Safe Memory-Error Repair Technical Papers Seongjoon Hong Korea University, Junhee Lee Korea University, South Korea, Jeongsoo Lee Korea University, Hakjoo Oh Korea University, South Korea | ||
08:44 12mTalk | 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 3mTalk | 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 | ||
09:10 - 10:00 | |||
09:10 50mTalk | 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 | ||