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): Sophia Drossopoulou, Aviral Goel
Fri 20 Nov 2020 19:00 - 19:20 at SPLASH-III - F-1B Chair(s): Steve Blackburn, Alex Potanin

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

Displayed time zone: Central Time (US & Canada) change

07:00 - 08:20
F-1BOOPSLA at SPLASH-III +12h
Chair(s): Sophia Drossopoulou Imperial College London, Aviral Goel Northeastern University
07:00
20m
Talk
Incremental Predicate Analysis for Regression Verification
OOPSLA
Qianshan Yu Tsinghua University, Fei He Tsinghua University, Bow-Yaw Wang Academia Sinica
Link to publication DOI Media Attached
07:20
20m
Talk
Learning Graph-Based Heuristics for Pointer Analysis without Handcrafting Application-Specific Features
OOPSLA
Minseok Jeon Korea University, Myungho Lee Korea University, Hakjoo Oh Korea University
Link to publication DOI Media Attached
07:40
20m
Talk
TacTok: Semantics-Aware Proof Synthesis
OOPSLA
Emily First University of Massachusetts at Amherst, Yuriy Brun University of Massachusetts Amherst, Arjun Guha University of Massachusetts at Amherst
Link to publication DOI Pre-print Media Attached
08:00
20m
Talk
Guiding Dynamic Programing via Structural Probability for Accelerating Programming by Example
OOPSLA
Ruyi Ji Peking University, Yican Sun Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
Link to publication DOI Media Attached
19:00 - 20:20
F-1BOOPSLA at SPLASH-III
Chair(s): Steve Blackburn Australian National University, Alex Potanin Victoria University of Wellington
19:00
20m
Talk
Incremental Predicate Analysis for Regression Verification
OOPSLA
Qianshan Yu Tsinghua University, Fei He Tsinghua University, Bow-Yaw Wang Academia Sinica
Link to publication DOI Media Attached
19:20
20m
Talk
Learning Graph-Based Heuristics for Pointer Analysis without Handcrafting Application-Specific Features
OOPSLA
Minseok Jeon Korea University, Myungho Lee Korea University, Hakjoo Oh Korea University
Link to publication DOI Media Attached
19:40
20m
Talk
TacTok: Semantics-Aware Proof Synthesis
OOPSLA
Emily First University of Massachusetts at Amherst, Yuriy Brun University of Massachusetts Amherst, Arjun Guha University of Massachusetts at Amherst
Link to publication DOI Pre-print Media Attached
20:00
20m
Talk
Guiding Dynamic Programing via Structural Probability for Accelerating Programming by Example
OOPSLA
Ruyi Ji Peking University, Yican Sun Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
Link to publication DOI Media Attached