Conditional Interpolation: Making Concurrent Program Verification More Effective
Wed 25 Aug 2021 23:10 - 23:20 - Analysis—Model Checking Chair(s): Matthew B Dwyer
Due to the state-space explosion problem, efficient verification of real-world programs in large scale is still a big challenge. Particularly, thread alternation makes the verification of concurrent programs much more difficult since it aggravates this problem. In this paper, an application of Craig interpolation, namely conditional interpolation, is proposed to work together with CEGAR-based approach to reduce the state-space of concurrent tasks. Specifically, conditional interpolation is formalized to confine the reachable region of states so that infeasible conditional branches could be pruned. Furthermore, the generated conditional interpolants are utilized to shorten the interpolation paths, which makes the time consumed for verification significantly reduced. We have implemented the proposed approach on top of an open-source software model checker. Empirical results show that the conditional interpolation is effective in improving the verification efficiency of concurrent tasks.
Wed 25 AugDisplayed time zone: Athens change
11:00 - 12:00 | Analysis—Model CheckingJournal First / Research Papers +12h Chair(s): Domenico Bianculli University of Luxembourg | ||
11:00 10mPaper | Checking LTL[F,G,X] on Compressed Traces in Polynomial Time Research Papers Minjian Zhang University of Illinois at Urbana-Champaign, Umang Mathur University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-Champaign DOI | ||
11:10 10mPaper | Conditional Interpolation: Making Concurrent Program Verification More Effective Research Papers DOI | ||
11:20 10mPaper | RegionTrack: A Trace-based Sound and Complete Checker to Debug Transactional Atomicity Violations and Non-Serializable Traces Journal First Xiaoxue Ma City University of Hong Kong, Shangru WU City University of Hong Kong, Ernest Pobee City University of Hong Kong, Xiupei Mei City University of Hong Kong, Hao Zhang City University of Hong Kong, Bo Jiang Beihang University, Wing-Kwong Chan City University of Hong Kong, Hong Kong | ||
11:30 30mLive Q&A | Q&A (Analysis—Model Checking) Research Papers |
23:00 - 00:00 | Analysis—Model CheckingResearch Papers / Journal First Chair(s): Matthew B Dwyer University of Virginia | ||
23:00 10mPaper | Checking LTL[F,G,X] on Compressed Traces in Polynomial Time Research Papers Minjian Zhang University of Illinois at Urbana-Champaign, Umang Mathur University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-Champaign DOI | ||
23:10 10mPaper | Conditional Interpolation: Making Concurrent Program Verification More Effective Research Papers DOI | ||
23:20 10mPaper | RegionTrack: A Trace-based Sound and Complete Checker to Debug Transactional Atomicity Violations and Non-Serializable Traces Journal First Xiaoxue Ma City University of Hong Kong, Shangru WU City University of Hong Kong, Ernest Pobee City University of Hong Kong, Xiupei Mei City University of Hong Kong, Hao Zhang City University of Hong Kong, Bo Jiang Beihang University, Wing-Kwong Chan City University of Hong Kong, Hong Kong | ||
23:30 30mLive Q&A | Q&A (Analysis—Model Checking) Research Papers |