alt Hacker NewsI'm curious about your workflow (or the one in the blog post), I have been doing some experiments proving things about existing binaries and it's been extremely slow progress.
I'm curious about your workflow (or the one in the blog post), I have been doing some experiments proving things about existing binaries and it's been extremely slow progress.
Yeah it took a bit to decide which abstraction level to target but I ended up choosing LLVM IR (planning to try PTX soon). It's been pretty successful so far for SIMD stuff, although proving theorems about concurrent programs seems a lot slower so far.