Comment by isaacfrond

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?