Hacker News Reader

On a related note, as far as I can tell the STOKE code seems to be incorrect w.r.t. aliasing between y and x, i.e. if x == y + 1. Makes me wonder what SMT solver claims are worth in the literature.

View on HN

I've worked with SMT solvers, Z3 in particular, before and it's definitely doable to prove two pieces of code equivalent, but that depends on the implementation used. Unfortunately, most academics, even when publishing at very influential conferences, rarely present their code for audit.

STOKE is on github here: https://github.com/StanfordPL/stoke.

Most CS conferences are making a big push towards "artifact evaluation," which means that many papers now come with peer-reviewed implementations.

Checking whether your code is correct under aliasing has nothing to do with the SMT solver. The solver can only analyze the model of the program given to it and it looks like the STOKE memory model assumes that the arguments don't alias.

Reply on news.ycombinator.com