Talk:Abstract interpretation

commercial products

The tools added by 212.82.36.34 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 212.82.36.34 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, 212.82.36.34 is refusing reverse DNS lookups, but from here www.aisee.com is resolving 212.82.32.59, 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:203.35.82.3 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 (talk • contribs) 20:36, 4 June 2012 (UTC)

Definition of "valid abstraction"

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 L₁, L₂, L′₁ and L′₂ be ordered sets. The concrete semantics f is a monotonic function from L₁ to L₂. A function f′ from L′₁ to L′₂ is said to be a valid abstraction of f if for all x′ in L′₁, (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 L₁ and L₂ should perhaps be explicitly clarified (the set of language terms and a semantic domain respectively?). The same remark holds for L₁ and L₂. 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)

CodeSonar

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)

The whole intuition section is awful

This does not aid understanding but rather merely rambles through cumbersome metaphors.

https://wiki.mozilla.org/Abstract_Interpretation explains the issue briefly but understandably without any metaphors. Instead it builds intuition via simplification.

I vote to just remove this section. It would be easier to just start over. — Preceding unsigned comment added by 107.15.224.170 (talk) 00:30, 21 April 2019 (UTC)

I was going to make the same comment. Very few people are able to write good tutorial introductions. This one is terrible -- it is not to the point, detracts from the true contribution of abstract interpretation, and, worse yet, uninteresting -- the reader doesn't learn anything useful.

Would agree with sheer removal.

Someone who really understands abstract interpretation should write a decent intro. ~~ Bangarmaine (talk) 09:22, 18 May 2022 (UTC)

I agree. The chosen example is used to illustrate some subtleties of abstract interpretation, but fails to explain the main motivation: to simplify infeasibly complex computation by falling back upon a simpler (more abstract) model, thereby accepting a loss of precision. I guess there are good examples outside the area of computer science, but no one came to my mind yet. - Jochen Burghardt (talk) 11:12, 18 May 2022 (UTC)

Indeed. I just wasted a paragraph of my life reading this section. All it says is that you can still reason about something when removing some of the information, potentially. Lets start with this intuition paragraph and remove it, please? 186.12.8.169 (talk) 18:33, 20 March 2024 (UTC)

Here we are 5 years later and it is still as horrible. For one thing, it does not describe AI in general but more something like abstraction in model-checking. It is also completely useless. I would replace it but I think a real AI expert would do it better. Please! (Note: AI = abstract interpretation here, now what others might think.) Bangarmaine (talk) 13:58, 2 November 2024 (UTC)

Tools section

The section "Tools" was deleted by MrOllie. I agree that is it a spam magnet, but completely deleting it is an inadequately hard measure. As a compromise, I suggest to allow only tools that

1. have an own wikipedia article (in particular: no external links), and
2. demonstrably employ abstract interpretation (in particular: no "Unsound tools"; they might belong at static program analysis, but not here).

In order to establish this as a strictly enforced policy, a wide consensus should be established here. - Jochen Burghardt (talk) 10:27, 22 January 2020 (UTC)