Abstraction-Guided Abstraction Simplification Export

@article{AbsGuidedAbs, abstract = {In abstract interpretation, approximation is encoded by abstract domains. Abstract domains provide a systematic guideline for defining abstract semantic functions as so-called best correct approximations of concrete semantic functions. However, it may happen that an abstract domain is unnecessarily too accurate for the specific purpose of approximating a given set of semantic functions. This work puts forward Abstraction-Guided Abstraction Simplification (AGAS), a methodology that allows to simplify abstract domains, i.e. to remove abstract values from them, in a maximal way while retaining exactly the same best correct approximations of concrete semantic functions. We show how AGAS can be applied in the context of abstract model checking by providing a simplification paradigm of abstract state spaces that can be viewed as a dual methodology to CounterExample-Guided Abstraction Refinement (CEGAR).}, archivePrefix = {arXiv}, author = {Giacobazzi, Roberto and Ranzato, Francesco}, citeulike-article-id = {6014594}, citeulike-linkout-0 = {http://arxiv.org/abs/0910.4748}, citeulike-linkout-1 = {http://arxiv.org/pdf/0910.4748}, day = {25}, eprint = {0910.4748}, keywords = {abstraction}, month = {Oct}, posted-at = {2009-10-27 07:29:45}, priority = {2}, title = {Abstraction-Guided Abstraction Simplification}, url = {http://arxiv.org/abs/0910.4748}, year = {2009} }

TY - JOUR ID - AbsGuidedAbs L3 - citeulike-article-id:6014594 N2 - In abstract interpretation, approximation is encoded by abstract domains. Abstract domains provide a systematic guideline for defining abstract semantic functions as so-called best correct approximations of concrete semantic functions. However, it may happen that an abstract domain is unnecessarily too accurate for the specific purpose of approximating a given set of semantic functions. This work puts forward Abstraction-Guided Abstraction Simplification (AGAS), a methodology that allows to simplify abstract domains, i.e. to remove abstract values from them, in a maximal way while retaining exactly the same best correct approximations of concrete semantic functions. We show how AGAS can be applied in the context of abstract model checking by providing a simplification paradigm of abstract state spaces that can be viewed as a dual methodology to CounterExample-Guided Abstraction Refinement (CEGAR). TI - Abstraction-Guided Abstraction Simplification KW - abstraction AU - Giacobazzi, Roberto AU - Ranzato, Francesco PY - 2009/Oct/25/ UR - http://arxiv.org/abs/0910.4748 ER -