Correctness Kernels of Abstract Interpretations

Details Correctness Kernels of Abstract Interpretations Correctness Kernels of Abstract Interpretations

2009-10-25

arxiv.org/abs/0910.4748v2

Computer Science

Programming Languages

An extended abstract of this paper appeared in Proceedings of the 37th International Colloquium on Automata, Languages, and Pr

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Correctness Kernels of Abstract Interpretations does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Correctness Kernels of Abstract Interpretations, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Correctness Kernels of Abstract Interpretations will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-450485