4 ms·
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
by Karrot_Kream 10y ago
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.
- 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.