High-Throughput, Formal-Methods-Assisted Fuzzing for LLVM [pdf]

Associated blog entry: <a href="https:&#x2F;&#x2F;blog.regehr.org&#x2F;archives&#x2F;2148" rel="nofollow">https:&#x2F;&#x2F;blog.regehr.org&#x2F;archives&#x2F;2148</a>

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?

Paper is very confusing if the past year had trained your brain to skip the V in LLVM.