Associated blog entry: https://blog.regehr.org/archives/2148

My goal for 2024 is to read as many John Regehr publications as I can.

Time well spent.

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?

Formal specification of LLVM and compile semantics to Z3, I would guess.

Pretty much this. It's called Alive2.

https://dl.acm.org/doi/abs/10.1145/3453483.3454030

tnanks

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

Consider getting a better model that doesn’t hallucinate like that.