It is based on separation logic. And apparently this makes it scale at the size of Facebook. IIRC, the tool runs in every commit. Also, I think each tool finds

It is based on separation logic. And apparently this makes it scale at the size of Facebook. IIRC, the tool runs in every commit. Also, I think each tool finds different bugs, they have a different set of false positives/negatives. So it’s good to be familiar with multiple tools.