Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Fri 31 May 2019 11:40 - 12:00 at St-Denis / Notre-Dame - Concurrency Chair(s): Tuba Yavuz

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 May

Displayed 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
20m
Talk
Safe Automated Refactoring for Intelligent Parallelization of Java 8 StreamsArtifacts AvailableTechnical 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
20m
Talk
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
20m
Talk
Parallel Refinement for Multi-Threaded Program VerificationArtifacts AvailableArtifacts Evaluated ReusableTechnical Track
Technical Track
Liangze Yin National University of Defense Technology, Wei Dong , Wanwei Liu National University of Defense Technology, Ji Wang
12:00
20m
Talk
SWORD: A Scalable Whole Program Race Detector for JavaDemos
Demonstrations
Yanze Li , Bozhen Liu Texas A&M University, USA, Jeff Huang Texas A&M University
12:20
10m
Talk
Discussion Period
Papers