Write a Blog >>
ESEC/FSE 2021
Thu 19 - Sat 28 August 2021 Clowdr Platform
Wed 25 Aug 2021 11:10 - 11:20 - Analysis—Model Checking Chair(s): Domenico Bianculli
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 Aug

Displayed time zone: Athens change

11:00 - 12:00
Analysis—Model CheckingJournal First / Research Papers +12h
Chair(s): Domenico Bianculli University of Luxembourg
11:00
10m
Paper
Checking LTL[F,G,X] on Compressed Traces in Polynomial TimeArtifacts AvailableArtifacts Reusable
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
10m
Paper
Conditional Interpolation: Making Concurrent Program Verification More Effective
Research Papers
Jie Su Xidian University, Cong Tian Xidian University, Zhenhua Duan Xidian University
DOI
11:20
10m
Paper
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
30m
Live 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
10m
Paper
Checking LTL[F,G,X] on Compressed Traces in Polynomial TimeArtifacts AvailableArtifacts Reusable
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
10m
Paper
Conditional Interpolation: Making Concurrent Program Verification More Effective
Research Papers
Jie Su Xidian University, Cong Tian Xidian University, Zhenhua Duan Xidian University
DOI
23:20
10m
Paper
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
30m
Live Q&A
Q&A (Analysis—Model Checking)
Research Papers