Abstract Interpretation in a Nutshell

by Nokinside on 10/26/2023, 5:48:07 PM with 14 comments

  • by nextos on 10/28/2023, 11:54:41 PM

    On the same topic, these lecture notes are pretty approachable: https://cs.au.dk/~amoeller/spa

    There is also this course, partially based on Cousot & Cousot, i.e. the OP: https://janmidtgaard.dk/aiws15

  • by agumonkey on 10/29/2023, 12:10:07 PM

    related http://web.mit.edu/16.399/www/ (https://archive.is/hxZUs)

  • by i_don_t_know on 10/29/2023, 10:06:18 AM

    See also chapter 6 of Program Analysis (an Appetizer) by Nielsen and Nielsen. Free PDF at https://arxiv.org/abs/2012.10086#

  • by dilawar on 10/29/2023, 2:52:51 AM

    This is very nice. Thanks for posting.

  • by bordercases on 10/29/2023, 12:46:56 AM

    Very good.

  • by gala8y on 10/29/2023, 8:05:24 AM

    Please, ELI5.

  • by _a_a_a_ on 10/29/2023, 11:13:34 AM

    It's the kind of thing that might make sense if you understood it, but that's hardly going to help a newbie. I also have some real doubt whether it's actually accurate or helpful. For instance

    "If an execution is represented by a curve showing the evolution of the vector x(t) of values of the input, state and output variables of the program as a function of the time t, this concrete semantics can be represented by a set of curves (with continuous time for short): x(t)"

    To call these curves is just weird, and suggest this could be plotted on a two-dimensional graph is hugely misleading (And 'continuous time'???)

    "The concrete semantics of a program is an "infinite" mathematical object which is not computable: it is not possible to write a program able to represent and to compute all possible executions of any program in all its possible execution environments"

    Really? Let's determine if a program halts, that can't be trivial can it. Here's my program:

        HALT;
    "In formal methods the abstract semantics must be chosen as a superset of the concrete semantics since otherwise reasonings in the abstract might not be correct in the concrete"

    By 'superset' I think he means a subset, or more restrictive, because otherwise you could have abstract semantics that allow more behaviour than the programming language. Or maybe it doesn't, but it's so bloody unclear that even I'm getting confused.

    etc.

    Abstract interpretation is an interest of mine (doesn't mean I know much about it though) and I think this post is a bloody mess.

    I will look at the references he's provided and also at the other links people here have posted (thanks). I hope his books are better than his blog.

    (Also AFAICT from the linked coures, this is circa 2005)