Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Predicting Lemmas in Generalization of IC3

Yuheng Su, Qiusong Yang, Yiwei Ci

TL;DR

This paper proposes a novel approach to predict a possible minimal lemma before dropping variables by utilizing the counterexample to propagation (CTP) and can avoid dropping variables if predict successfully.

Abstract

The IC3 algorithm, also known as PDR, has made a significant impact in the field of safety model checking in recent years due to its high efficiency, scalability, and completeness. The most crucial component of IC3 is inductive generalization, which involves dropping variables one by one and is often the most time-consuming step. In this paper, we propose a novel approach to predict a possible minimal lemma before dropping variables by utilizing the counterexample to propagation (CTP). By leveraging this approach, we can avoid dropping variables if predict successfully. The comprehensive evaluation demonstrates a commendable success rate in lemma prediction and a significant performance improvement achieved by our proposed method.

Predicting Lemmas in Generalization of IC3

TL;DR

This paper proposes a novel approach to predict a possible minimal lemma before dropping variables by utilizing the counterexample to propagation (CTP) and can avoid dropping variables if predict successfully.

Abstract

The IC3 algorithm, also known as PDR, has made a significant impact in the field of safety model checking in recent years due to its high efficiency, scalability, and completeness. The most crucial component of IC3 is inductive generalization, which involves dropping variables one by one and is often the most time-consuming step. In this paper, we propose a novel approach to predict a possible minimal lemma before dropping variables by utilizing the counterexample to propagation (CTP). By leveraging this approach, we can avoid dropping variables if predict successfully. The comprehensive evaluation demonstrates a commendable success rate in lemma prediction and a significant performance improvement achieved by our proposed method.

Paper Structure

This paper contains 14 sections, 3 theorems, 6 equations, 4 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Basics and Notations
  4. Overview of IC3
  5. Predicting Lemmas
  6. Intuition
  7. How to Refine Cubes
  8. The Algorithm
  9. Evaluation
  10. Experimental Setup
  11. Experimental Results
  12. Analysis
  13. Related Work
  14. Conclusion and Future Work

Key Result

theorem 1

Let $a$ and $b$ are cubes, $a \neq \bot$ and $b \neq \bot$. $a \land b = \bot$, iff $diff(a, b) \neq \emptyset$.

Figures (4)

  • Figure 1: $F_{i-1}$ and $F_i$ frames: the square represents the entire state space, the blue region represents the state space represented by the frame, and each triangle in the purple region represents states blocked by a cube.
  • Figure 2: Comparisons among the different configurations.
  • Figure 3: Scatters of RIC3 and IC3ref with and without the proposed optimization. Points below the diagonal indicate better performance with the proposed optimization active.
  • Figure 4: Comparing the ratio of runtime of different implementations without and with our proposed optimization (left y-axis) with the success rate of avoiding dropped variables $SR_{adv}$ during generalization (x-axis). The right y-axis represents the cumulative number of cases with improved performance as the prediction accuracy increases. Cases with runtime both timeout or both less than 1s are ignored.

Theorems & Definitions (4)

  • definition 1: Diff Set
  • theorem 1
  • theorem 2
  • theorem 3