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 an abstract interpretation, 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

Correctness Kernels of Abstract Interpretations

GIACOBAZZI, Roberto;
2014-01-01

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 an abstract interpretation, 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
2014
Abstract domains; Abstract interpretations; Abstract model-checking; Abstract semantics; Concrete system; Counterexample-guided abstraction refinement; Semantic functions
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/930497
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 3
social impact