4 ms·
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 solve
by wohlergehen 10y ago
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.
- Karrot_Kream 10y agoI'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.
- wsxcde 10y agoSTOKE is on github here: https://github.com/StanfordPL/stoke 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.
- wsxcde 10y agoChecking 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.