Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study

Rafael Sá Menezes, Edoardo Manino, Fedor Shmarov, Mohannad Aldughaim, Rosiane de Freitas, Lucas C. Cordeiro

TL;DR

This work evaluates whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use, and shows that interval analysis is essential in solving 203 unique benchmarks.

Abstract

Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack of completeness. Over the years, interval analysis has repeatedly been proposed as a partial solution to these limitations. In this work, we evaluate whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use. In more detail, we quantify the benefits of interval analysis on two benchmarks: the Intel Core Power Management firmware and 9537 programs in the ReachSafety category of the International Competition on Software Verification. Our results show that interval analysis is essential in solving 203 unique benchmarks.

Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study

TL;DR

This work evaluates whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use, and shows that interval analysis is essential in solving 203 unique benchmarks.

Abstract

Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack of completeness. Over the years, interval analysis has repeatedly been proposed as a partial solution to these limitations. In this work, we evaluate whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use. In more detail, we quantify the benefits of interval analysis on two benchmarks: the Intel Core Power Management firmware and 9537 programs in the ReachSafety category of the International Competition on Software Verification. Our results show that interval analysis is essential in solving 203 unique benchmarks.
Paper Structure (22 sections, 3 equations, 4 figures, 2 algorithms)

This paper contains 22 sections, 3 equations, 4 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Bounded Model Checking (BMC)
  4. Interval Analysis
  5. Computing Intervals through Abstract Interpretation
  6. Integer Domain ($\mathbb{I}$)
  7. Wrapped Domain ($\mathbb{W}$)
  8. Boolean Domain
  9. Computing Intervals
  10. GOTO language
  11. Program safety
  12. Abstract Domains for GOTO
  13. Initializing the Domain ($\textbf{Init}_\alpha$)
  14. Transforming the Domain ($\textbf{Transform}_\alpha$)
  15. Joining Intervals ($\textbf{Join}_\alpha$)
  16. ...and 7 more sections

Figures (4)

  • Figure 1: Interval analysis of a program. On the left: a program with operations over the variable x, and on the right: the computed intervals.
  • Figure 2: Abstract Domains.
  • Figure 3: Domain data structures. (a) a data structure that stores intervals for all variables and statements; (b) a data structure where the intervals are shared between all statements to avoid redundancy; (c) a data structure that improves over (b) by sharing groups of intervals.
  • Figure 4: The ESBMC architecture with interval analysis.