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)

Verification revert

@Jochen Burghardt: Hi, I noticed that my recent edit adding software verification as an application of abstract interpretation was reverted with the summary "not mentioned in target page".

Is this because the linked article on software verification doesn't include abstract interpretation? Source wise, this claim is supported by Cousot and Cousot's original 1977 paper, among others (my understanding is that this application is widely used today). Would you support readding it with citation? I'd appreciate clarification before making further changes. Thanks! Hijiri Suzuki (talk) 17:19, 10 October 2026 (UTC)

Yes, my reason was that I couldn't find any mention of abstract interpretation in the Software verification page. Moreover, before my retirement, I worked in both the field of abstract interpretation and that of software verification, and always found them separated approaches (e.g. in the Frama-C family: "EVA" for abstract interpretation, "WP" for Hoare-style verification). The Cousots may have suggested verification as a possible future application when they devised their approach in 1977, but I never saw a corresponding implementation. - Jochen Burghardt (talk) 10:10, 11 October 2026 (UTC)

Thanks for the clarification! I think in my mind, Hoare style verification was not necessarily the same as software verification (for instance there are some papers that treat EVA as a potential application to software verification). To a less specific extent, Cousot (somewhat) recently had a talk at PPDP on the applications to program verification, which I know is not quite the same but are closely related.

I think that this problem is probably sufficiently specific enough that I'm willing to agree with the idea that at the moment they're probably enough separated to not warrant putting it in the article. I initially put it in because I had recently seen some work at OOPSLA related to applications of absint in software verification, but this is also so recent that this may take a few years to become reasonably relevant. Hijiri Suzuki (talk) 05:24, 13 October 2026 (UTC)