---
abstract: 'In static analysis, approximation is typically encoded by abstract domains, providing systematic guidelines for specifying approximate semantic functions and precision assessments. However, it may happen that an abstract domain contains redundant information for the specific purpose of approximating a given semantic function modeling some behavior of a system. This paper introduces correctness kernels 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 and predicate abstraction, correctness kernels provide a simplification paradigm of the abstract state space that is guided by examples, meaning that it 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.'
author:
- '[Roberto Giacobazzi       Francesco Ranzato]{}'
title: Correctness Kernels of Abstract Interpretations
---

Introduction {#intro}
============

In static analysis and verification, model-driven *abstraction refinement* has emerged in the last decade as a fundamental method for improving abstractions towards more precise yet efficient analyses. The basic idea is simple: given an abstraction modeling some observational behavior of the system to analyze, refine 