In static analysis, approximation is typically encoded by abstract domains, providing systematic guidelines for specifying approximate semantic functions and precision assessments. However, it may well 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 Example-Guided Abstraction Simplification (EGAS), 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, EGAS provides 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 EGAS can be integrated with the well-known CEGAR (CounterExample-Guided Abstraction Refinement) methodology.

Example-guided abstraction simplification

RANZATO, FRANCESCO
2010

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 well 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 Example-Guided Abstraction Simplification (EGAS), 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, EGAS provides 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 EGAS can be integrated with the well-known CEGAR (CounterExample-Guided Abstraction Refinement) methodology.
2010
Automata, Languages and Programming, 37th International Colloquium, ICALP 2010
37th International Colloquium on Automata, Languages and Programming (ICALP 2010)
9783642141614
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/11577/2420369
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 3
  • OpenAlex ND
social impact