[joelburget]

Co-author here. We're planning to turn this into a series, with additional posts on how symbolic execution works at a lower level, how to present counterexamples to users, and ideas for future programming tools built on symbolic execution.

[dfabulich]

One piece of feedback: I've often wished to work on static analysis tools, but too much of the work in this area is focused on Haskell or Lisp. (All of the code in this article is in Haskell or Lisp.)

Does any of this stuff work on Java, Python, or JavaScript? I want to improve the quality of real-world programs written in industry-standard languages.

This "gentle introduction" makes it seem like the first step of the process is "port your app to a homoiconic language," -- or, in other words, "you can prove the correctness of any language you want, as long as it's Haskell or Lisp."

[nickpsecurity]

https://en.wikipedia.org/wiki/List_of_tools_for_static_code_...

[dfabulich]

That's static analysis, but not symbolic execution. Looking at the JavaScript section, you can't do any of the stuff described in the article with JSLint.

[tluyben2]

Abstract interpretation is a wider concept than symbolic execution; check the post in the top thread answered by user mjn to get more info; the fb and mozilla ones seem to focus on more mainstream languages.

[nickpsecurity]

The parent said "static analysis" tools. That's what I gave them.

[sophiebits]

Prepack is an example of a (not production ready) tool to do abstract evaluation of JS.

[CalChris]

Seriously helpful article. Looking forward to the sequels.

  we can map each syntax tree to an interpreter

Maybe I'm being dense but I'm not sure what you mean by map here. A map is from set to set. I'm not thinking of an interpreter as a set.

[joelburget]

I'll use a bit of Haskell in my response, since that's what I'm most comfortable with and what we actually use for our work. Hopefully that's okay.

We can define a data type of expressions in our language, with addition, multiplication, etc.

  data Expr = Addition Expr Expr | Multiplication Expr Expr | ...

Then we need the type of an interpreter which consumes program inputs and produces an output. I'll leave this abstract for now.

  data Interpreter = ...

By map, we just mean that we can write a Haskell function with this type

  interpret :: Expr -> Interpreter
  interpret (Addition a b) = (+) <$> interpret a <*> interpret b
  interpret (Multiplication a b) = (*) <$> interpret a <*> interpret b

If you're curious, here's some real symbolic evaluation code I wrote doing the same https://github.com/kadena-io/pact/blob/234ba3dd01f0df8b4e462...

[CalChris]

Well, I'm glad I asked. I get this now. It really is a mapping. But this was a bit of shorthand that I didn't get in the post. You might want to add that.

[Xophmeister]

The set of interpreters.