Talk:Abstract interpretation

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Computer science (Rated Start-class, Mid-importance)
WikiProject icon This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Start-Class article Start  This article has been rated as Start-Class on the project's quality scale.
 Mid  This article has been rated as Mid-importance on the project's importance scale.

commercial products[edit]

The tools added by to this page refer to the commercial products of one (or two?) compiler vendor(s?). People in the program analysis research community do not consider these tools to be "standards" of any kind; there are dozens or hundreds of little compiler vendors in the world; these particular links are of little more encyclopedic interest than, say, your neighborhood plumber's web site. Hence, linking them up here may not be appropriate. At least, they should be clearly labeled as one set of commercial tools among many. See also similar edit to Optimization (computer science). k.lee 06:59, 15 Aug 2003 (UTC)

Be they spam or not, if they're obscure products, they shouldn't be listed unless those famous ones are listed as well. --Menchi 06:40, Aug 19, 2003 (UTC)

Update: It appears that all of the contributions made on August 14 by are links to commercial products by the same company, AbsInt. See, e.g., the edit to dinosaur --- in this case the page that it links to isn't even very informative: you have to click special links to get any graph that actually gives you any information, and the only complete version of the linked graph is in formats that most users will not be able to view.

Additionally, is refusing reverse DNS lookups, but from here is resolving, which is on the same subnet. I now strongly suspect that this is spam, or at least a well-meaning but misguided individual affiliated with this company. k.lee 07:08, 15 Aug 2003 (UTC)

Two relevant points from the What Wikipedia is not page

  • Mere collections of external links. (But of course there's nothing wrong with adding both lists of links and lists of on-line references you used in writing an article.)
  • A vehicle for advertising. We don't need articles on items just because a contributor is associated with them. However, commercial links are certainly OK if they can serve to identify major corporations associated with a topic.

And from the talk page of What Wikipedia is not;

  • Do we have a policy on users who merely spend their time adding weblinks to one company, presumably in an attempt at promotion? For example, user: has added lots of e-text external links to the same company - how to handle this? Martin
  • In this case, I think the links should be replaced with links to a non-commercial source (e.g. Gutenberg) ASAP, but they're OK for the time being. What would be a reason for banning is if he replaced links to non-commercial sources with commercial ones. --Eloquence 19:00 Feb 27, 2003 (UTC)

Angela 01:00, 19 Aug 2003 (UTC)

If the tools are non-standard, they should go, I reckon. Martin 13:57, 24 Aug 2003 (UTC)

AbsInt makes fairly interesting abstract interpretation-based static analysis tools, but they're not the only ones and their tools are not "standard" in any way. David.Monniaux 08:35, 22 Apr 2004 (UTC)

In case you refer to Astreé, the development is lead by Cousot himself. Who defines what "standard" is? — Preceding unsigned comment added by Borishollas (talkcontribs) 20:36, 4 June 2012 (UTC)

Definition of "valid abstraction"[edit]

There is a problem with this definition: the function γ is not defined or quantified over, so we have no idea what it is. From notation used in the preceding paragraph, I would presume it's a concretization function, but we don't know.

Let L1, L2, L1 and L2 be ordered sets. The concrete semantics f is a monotonic function from L1 to L2. A function f′ from L1 to L2 is said to be a valid abstraction of f if for all x′ in L1, (f ∘ γ)(x′) ≤ (γ ∘ f′)(x′).

--saf 06:32, 19 October 2006 (UTC)

Even by assuming that γ is a concretization function, which is consistent with the previous definitions, the definition of "valid abstraction" remains problematic. If γ is a concretization function it should have an abstract set as source and its corresponding concrete one as a target. But f has a concrete set as a target, so f cannot be composed with γ as in the definition. Also, the meaning of L1 and L2 should perhaps be explicitly clarified (the set of language terms and a semantic domain respectively?). The same remark holds for L1 and L2. Finally, one would possibly expect a pair of abstraction/concretization functions for both pairs of concrete/abstract sets, and a clear stating of whether α and γ are between the pair with subscript 1 or that with subscript 2 (the compositions with f and f′ in the definition suggest that the second case holds). Pietro Braione 18:47, 4 January 2007 (UTC)

The composition is correct, the definition is consistent. But indeed it lacks in clarity. Tomdo08 (talk) 20:10, 6 April 2013 (UTC)
... also the definition of valid abstraction is suspiciously narrow: It seems to only be good for bounding. Tomdo08 (talk) 20:16, 6 April 2013 (UTC)

The definition does seem narrow, and most information needs sources. Some paragraphs have only one external source while other paragraphs has one every other sentence. Ros215 (talk) 04:36, 19 April 2017 (UTC)


I sent an email to GrammaTech and they told me that CodeSonar does not use AI. So I removed it from the list of tools.--Borishollas (talk) 17:22, 2 June 2013 (UTC)