Parallel Refinement for Multi-Threaded Program VerificationTechnical Track
Program verification is one of the most important approaches to ensure the correctness of concurrent programs. However, due to the path explosion problem, concurrent program verification is usually time consuming, which significantly limits its scalability to industrial programs. Parallel processing is the most efficient technique to deal with those problems which require mass computing. Hence, designing parallel algorithms to improve the performance of concurrent program verification is highly desired. This paper focuses on parallelization of the abstraction refinement technique, one of the most efficient techniques for concurrent program verification. We have proposed a parallel refinement framework which employs multiple engines to refine the abstraction in parallel. Different from existing work which usually parallelizes the search process, our method achieves the effect of parallelization by refinement constraint and learnt clause sharing, such that the number of required iterations can be significantly reduced and the performance of constraint solving can be improved. We have implemented this framework on the scheduling constraint based abstraction refinement method, one of the best methods for concurrent program verification. Experimental results on SV-COMP 2018 show encouraging results of our method. For those complex cases requiring a large number of iterations, our method can obtain a linear reduce of the iteration number and significantly improve the verification performance.
Fri 31 MayDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:30 | ConcurrencyTechnical Track / Demonstrations / Papers at St-Denis / Notre-Dame Chair(s): Tuba Yavuz University of Florida | ||
11:00 20mTalk | Safe Automated Refactoring for Intelligent Parallelization of Java 8 StreamsTechnical TrackIndustry Program Technical Track Raffi Khatchadourian City University of New York (CUNY) Hunter College, Yiming Tang City University of New York (CUNY) Graduate Center, Mehdi Bagherzadeh Oakland University, Syed Ahmed Oakland University Pre-print Media Attached | ||
11:20 20mTalk | Detecting Atomicity Violations for Event-Driven Node.js ApplicationsTechnical TrackIndustry Program Technical Track Xiaoning Chang Institute of Software, Chinese Academy of Sciences, Wensheng Dou Institute of Software, Chinese Academy of Sciences, Yu Gao Institute of Software, Chinese Academy of Sciences, China, Jie Wang Institute of Software, Chinese Academy of Sciences, Jun Wei Institute of Software, Chinese Academy of Sciences, China, Tao Huang Institute of Software Chinese Academy of Sciences | ||
11:40 20mTalk | Parallel Refinement for Multi-Threaded Program VerificationTechnical Track Technical Track Liangze Yin National University of Defense Technology, Wei Dong , Wanwei Liu National University of Defense Technology, Ji Wang | ||
12:00 20mTalk | SWORD: A Scalable Whole Program Race Detector for JavaDemos Demonstrations | ||
12:20 10mTalk | Discussion Period Papers |