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 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Giacobazzi, R., & Ranzato, F. (2010). Example-guided abstraction simplification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6199 LNCS, pp. 211–222). https://doi.org/10.1007/978-3-642-14162-1_18
Mendeley helps you to discover research relevant for your work.