|Abstract Interpretation vs DFA in Clang and GCC firstname.lastname@example.org (Jack Smith) (2011-01-10)|
|Re: Abstract Interpretation vs DFA in Clang and GCC email@example.com (2011-01-17)|
|Re: Abstract Interpretation vs DFA in Clang and GCC firstname.lastname@example.org (Jack Smith) (2011-02-09)|
|Re: Abstract Interpretation vs DFA in Clang and GCC email@example.com (2011-02-15)|
|From:||firstname.lastname@example.org (Torben Ęgidius Mogensen)|
|Date:||Mon, 17 Jan 2011 12:14:33 +0100|
|Organization:||SunSITE.dk - Supporting Open source|
|Posted-Date:||18 Jan 2011 01:01:22 EST|
Jack Smith <email@example.com> writes:
> since someone says that nowadays it's better abstract interpretation
> than DFA can anyone tell me what's the difference among them?
Abstract interpretation (AI) has a strong tie to the semantics of the
language: Each value in AI corresponds to a set of values in the
semantics, which makes it relatively easy to prove the correctness of
an anlysis. Values in data-flow analysis (DFA) do not have such a
clear relation to the semantics, so they are more difficult to prove
correct. On the other hand, DFA can do analyses that are difficult to
express as AI, such as liveness. To do liveness analysis with AI you
need a continuation-passing semantics.
A more precise relation between the two can be found in the following
Schmidt, D.A. Data-flow analysis is model checking of abstract
interpretations. Proc. 25th ACM Symp. Principles of Programming
Languages, San Diego, 1998.
Schmidt, D.A. and Steffen, B. Data-flow analysis as model checking of
abstract interpretations. Proc. 5th Static Analysis Symposium,
G. Levi. ed., Pisa, September, 1998. Springer LNCS 1503.
Return to the
Search the comp.compilers archives again.