SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 07:00 - 07:20 at SPLASH-III - F-1B Chair(s): Aviral Goel, Sophia Drossopoulou
Fri 20 Nov 2020 19:00 - 19:20 at SPLASH-III - F-1B Chair(s): Alex Potanin, Steve Blackburn

Software products are evolving during their life cycles. Ideally, every revision need be formally verified to ensure software quality. Yet repeated formal verification requires significant computing resources. Verifying each and every revision can be very challenging. It is desirable to ameliorate regression verification for practical purposes. In this paper, we regard predicate analysis as a process of assertion annotation. Assertion annotations can be used as a certificate for the verification results. It is thus a waste of resources to throw them away after each verification. We propose to reuse the previously-yielded assertion annotation in regression verification. A light-weight impact-analysis technique is proposed to analyze the reusability of assertions. A novel assertion strengthening technique is furthermore developed to improve reusability of annotation. With these techniques, we present an incremental predicate analysis technique for regression verification. Correctness of our incremental technique is formally proved. We performed comprehensive experiments on revisions of Linux kernel device drivers. Our technique outperforms the state-of-the-art program verification tool CPAchecker by getting 2.8x speedup in total time and solving additional 393 tasks.

Fri 20 Nov
Times are displayed in time zone: Central Time (US & Canada) change

07:00 - 08:20: F-1BOOPSLA at SPLASH-III +12h
Chair(s): Aviral GoelNortheastern University, Sophia DrossopoulouImperial College London
07:00 - 07:20
Talk
OOPSLA
Qianshan YuTsinghua University, Fei HeTsinghua University, Bow-Yaw WangAcademia Sinica
Link to publication DOI Media Attached
07:20 - 07:40
Talk
OOPSLA
Minseok JeonKorea University, Myungho LeeKorea University, Hakjoo OhKorea University
Link to publication DOI Media Attached
07:40 - 08:00
Talk
OOPSLA
Emily FirstUniversity of Massachusetts at Amherst, Yuriy BrunUniversity of Massachusetts Amherst, Arjun GuhaUniversity of Massachusetts at Amherst
Link to publication DOI Pre-print Media Attached
08:00 - 08:20
Talk
OOPSLA
Ruyi JiPeking University, Yican SunPeking University, Yingfei XiongPeking University, Zhenjiang HuPeking University
Link to publication DOI Media Attached
19:00 - 20:20: F-1BOOPSLA at SPLASH-III
Chair(s): Alex PotaninVictoria University of Wellington, Steve BlackburnAustralian National University
19:00 - 19:20
Talk
OOPSLA
Qianshan YuTsinghua University, Fei HeTsinghua University, Bow-Yaw WangAcademia Sinica
Link to publication DOI Media Attached
19:20 - 19:40
Talk
OOPSLA
Minseok JeonKorea University, Myungho LeeKorea University, Hakjoo OhKorea University
Link to publication DOI Media Attached
19:40 - 20:00
Talk
OOPSLA
Emily FirstUniversity of Massachusetts at Amherst, Yuriy BrunUniversity of Massachusetts Amherst, Arjun GuhaUniversity of Massachusetts at Amherst
Link to publication DOI Pre-print Media Attached
20:00 - 20:20
Talk
OOPSLA
Ruyi JiPeking University, Yican SunPeking University, Yingfei XiongPeking University, Zhenjiang HuPeking University
Link to publication DOI Media Attached