Incremental predicate analysis for regression verification

• Published in: Proceedings of ACM on programming languages 2020-11, Vol.4 (OOPSLA), p.1-25, Article 184
• Main Authors: Yu, Qianshan, He, Fei, Wang, Bow-Yaw
• Format: Article
• Language: English
• Subjects: Formal software verification; Logic; Logic and verification; Software and its engineering; Software creation and management; Software verification and validation; Theory of computation
• ISSN: 2475-1421; 2475-1421
• DOI: 10.1145/3428252

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.