3 ms·
After scanning the paper and blog post, I miss what formal methods they are using. Apparently they have a system that given two source code fragments can proof
by isaacfrond 3y ago
After scanning the paper and blog post, I miss what formal methods they are using. Apparently they have a system that given two source code fragments can proof they are not equivalent. What are they using for that?
- quazar 3y agoFormal specification of LLVM and compile semantics to Z3, I would guess.
- boomanaiden154 3y agoPretty much this. It's called Alive2. https://dl.acm.org/doi/abs/10.1145/3453483.3454030 https://dl.acm.org/doi/abs/10.1145/3453483.3454030
- isaacfrond 3y agotnanks