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.

Conference Day
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 YavuzUniversity of Florida
Safe Automated Refactoring for Intelligent Parallelization of Java 8 StreamsArtifacts AvailableTechnical TrackIndustry Program
Technical Track
Raffi KhatchadourianCity University of New York (CUNY) Hunter College, Yiming TangCity University of New York (CUNY) Graduate Center, Mehdi BagherzadehOakland University, Syed AhmedOakland University
Pre-print Media Attached
Detecting Atomicity Violations for Event-Driven Node.js ApplicationsTechnical TrackIndustry Program
Technical Track
Xiaoning ChangInstitute of Software, Chinese Academy of Sciences, Wensheng DouInstitute of Software, Chinese Academy of Sciences, Yu GaoInstitute of Software, Chinese Academy of Sciences, China, Jie WangInstitute of Software, Chinese Academy of Sciences, Jun WeiInstitute of Software, Chinese Academy of Sciences, China, Tao HuangInstitute of Software Chinese Academy of Sciences
Parallel Refinement for Multi-Threaded Program VerificationArtifacts AvailableArtifacts Evaluated ReusableTechnical Track
Technical Track
Liangze YinNational University of Defense Technology, Wei Dong, Wanwei LiuNational University of Defense Technology, Ji Wang
SWORD: A Scalable Whole Program Race Detector for JavaDemos
Yanze Li, Bozhen LiuTexas A&M University, USA, Jeff HuangTexas A&M University
Discussion Period