Proof-Guided Underapproximation Widening for Bounded Model Checking

EasyChair Preprint 8344

Abstract

Bounded Model Checking (BMC) is a popularly used strategy for program verification and it has been explored extensively over the past decade. Despite such a long history, BMC still faces scalability challenges as programs continue to grow larger and more complex. One approach that has proven to be effective in verifying large programs is called Counter Example Guided Abstraction Refinement (CEGAR). In this work, we propose a complimentary approach to CEGAR. Our strategy works by gradually widening the underapproximation of a program, following proofs of unsatisfiability. We have implemented our ideas in a tool called LEGION. We compare the performance of LEGION against that of CORRAL, a state-of-the-art verifier from Microsoft, that utilizes the CEGAR strategy. We conduct our experiments on 727 Windows and Linux device driver benchmarks. We find that LEGION is able to solve 12% more instances than CORRAL and that LEGION exhibits a complementary behavior to that of CORRAL. Motivated by this, we also build a portfolio verifier, LEGION+, that attempts to draw the best of LEGION and CORRAL. Our portfolio, LEGION+, solves 15% more benchmarks than CORRAL with similar computational resource constraints (i.e. each verifier in the portfolio is run with a time budget that is half of the time budget of CORRAL). Moreover, it is found to be 2.9 times faster than CORRAL on benchmarks that are solved by both CORRAL and LEGION+.

Keyphrases: Bounded Model Checking, Underapproximation widening, software verification

@booklet{EasyChair:8344,
  author    = {Prantik Chatterjee and Jaydeepsinh Meda and Akash Lal and Subhajit Roy},
  title     = {Proof-Guided Underapproximation Widening for Bounded Model Checking},
  howpublished = {EasyChair Preprint 8344},
  year      = {EasyChair, 2022}}