Correctness Kernels of Abstract Interpretations

TL;DR

This paper introduces correctness kernels, a method for simplifying abstract domains in static analysis by removing redundant information while preserving the analysis's accuracy, and demonstrates their integration with CEGAR.

Contribution

It formalizes correctness kernels for abstract interpretation, providing a systematic way to simplify abstract domains without losing precision, and connects this approach with CEGAR.

Findings

Correctness kernels preserve the exact behavior of the original abstract interpretation.

They enable maximal simplification of abstract domains while maintaining analysis accuracy.

The approach integrates effectively with CEGAR, guiding the abstraction refinement process.

Abstract

In abstract interpretation-based static analysis, approximation is encoded by abstract domains. They provide systematic guidelines for designing abstract semantic functions that approximate some concrete system behaviors under analysis. It may happen that an abstract domain contains redundant information for the specific purpose of approximating a given concrete semantic function. This paper introduces the notion of correctness kernel of abstract interpretations, a methodology for simplifying abstract domains, i.e. removing abstract values from them, in a maximal way while retaining exactly the same approximate behavior of the system under analysis. We show that in abstract model checking correctness kernels provide a simplification paradigm of the abstract state space that is guided by examples, meaning that this simplification preserves spuriousness of examples (i.e., abstract paths). In particular, we show how correctness kernels can be integrated with the well-known CEGAR (CounterExample-Guided Abstraction Refinement) methodology.