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 NovDisplayed 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 20mTalk | Incremental Predicate Analysis for Regression Verification OOPSLA Link to publication DOI Media Attached | ||
07:20 20mTalk | Learning Graph-Based Heuristics for Pointer Analysis without Handcrafting Application-Specific Features OOPSLA Link to publication DOI Media Attached | ||
07:40 20mTalk | 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 20mTalk | 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 20mTalk | Incremental Predicate Analysis for Regression Verification OOPSLA Link to publication DOI Media Attached | ||
19:20 20mTalk | Learning Graph-Based Heuristics for Pointer Analysis without Handcrafting Application-Specific Features OOPSLA Link to publication DOI Media Attached | ||
19:40 20mTalk | 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 20mTalk | 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 |