4 ms·

Abstract Interpretation in a Nutshell

59 points by Nokinside 3y ago

nextos 3y ago
On the same topic, these lecture notes are pretty approachable: https://cs.au.dk/~amoeller/spa https://cs.au.dk/~amoeller/spa There is also this course, partially based on Cousot & Cousot, i.e. the OP: https://janmidtgaard.dk/aiws15 https://janmidtgaard.dk/aiws15
- anonymousDan 3y ago
  Converesely if you want a weighty tome on the matter see this recent book by Cousot: https://www.amazon.com/Principles-Abstract-Interpretation-Patrick-Cousot/dp/0262044900 https://www.amazon.com/Principles-Abstract-Interpretation-Pa...
  - nextos 3y ago
    Or Nielson & Nielson, discussed previously in HN: https://link.springer.com/book/10.1007/978-3-662-03811-6 https://link.springer.com/book/10.1007/978-3-662-03811-6
bordercases 3y ago
Very good.
dilawar 3y ago
This is very nice. Thanks for posting.
gala8y 3y ago
Please, ELI5.
i_don_t_know 3y ago
See also chapter 6 of Program Analysis (an Appetizer) by Nielsen and Nielsen. Free PDF at https://arxiv.org/abs/2012.10086# https://arxiv.org/abs/2012.10086#
_a_a_a_ 3y ago
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)
- samth 3y ago
  This article is by one of the two inventors of abstract interpretation. Maybe you didn't find it helpful but it is definitely accurate.
- bazoom42 3y ago
  > Really? Let's determine if a program halts, that can't be trivial can it. I don’t know if you are trolling, but the halting problem is the problem of an algorithm to detemine whether any arbitrary program halts.
  - deleted 3y ago
    [deleted]
agumonkey 3y ago
related http://web.mit.edu/16.399/www/ http://web.mit.edu/16.399/www/ (https://archive.is/hxZUs https://archive.is/hxZUs)
- _a_a_a_ 3y ago
  It's 'related' in that it's exactly the same course given in the link, specifically [10] at the end, thanks.

59 points by Nokinside 3y ago

On the same topic, these lecture notes are pretty approachable: https://cs.au.dk/~amoeller/spa https://cs.au.dk/~amoeller/spa There is also this course, partially based on Cousot & Cousot, i.e. the OP: https://janmidtgaard.dk/aiws15 https://janmidtgaard.dk/aiws15

anonymousDan 3y ago
Converesely if you want a weighty tome on the matter see this recent book by Cousot: https://www.amazon.com/Principles-Abstract-Interpretation-Patrick-Cousot/dp/0262044900 https://www.amazon.com/Principles-Abstract-Interpretation-Pa...
- nextos 3y ago
  Or Nielson & Nielson, discussed previously in HN: https://link.springer.com/book/10.1007/978-3-662-03811-6 https://link.springer.com/book/10.1007/978-3-662-03811-6

bordercases 3y ago

Very good.

dilawar 3y ago

This is very nice. Thanks for posting.

gala8y 3y ago

Please, ELI5.

i_don_t_know 3y ago

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

_a_a_a_ 3y ago

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)

samth 3y ago
This article is by one of the two inventors of abstract interpretation. Maybe you didn't find it helpful but it is definitely accurate.
bazoom42 3y ago
> Really? Let's determine if a program halts, that can't be trivial can it. I don’t know if you are trolling, but the halting problem is the problem of an algorithm to detemine whether any arbitrary program halts.
- deleted 3y ago
  [deleted]

agumonkey 3y ago

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

_a_a_a_ 3y ago
It's 'related' in that it's exactly the same course given in the link, specifically [10] at the end, thanks.