> How does this make no sense? Because most correctness properties aren't compositional. > What? You state that proving doesn't scale referring to constraint

> How does this make no sense? Because most correctness properties aren't compositional. > What? You state that proving doesn't scale referring to constraint based solutions? Sure, they don't scale. No, you've misunderstood the paper, and missed the part of the post where I provide necessary context. Like a lot of work in computational complexity theory, they're referring to the model checking problem, i.e. the problem of determining whether a program satisfies some property, not to any particular verification algorithm. Their results apply to all methods (their proofs don't not rely on any particular verification method but show hardness results). Also, it's funny that you say "they don't scale." You're right, none of the formal methods we have scales nearly as well as we'd like, to the point we can say "they don't scale" [1]. Of them, the one that scales the least is deductive proofs. That's the main reason it's the formal methods that is used the least. > constraint based solutions I don't know what you mean by that (SMT?), and I don't recall mentioning those. > Because you can automate anything you can prove with a SMT or model checker? Yes, model checkers are completely automatic. SMT is a class of algorithms and techniques used in various verification methods -- deductive proofs, model checking, static analysis, concolic testing -- not a verification method in itself, so I'm not sure what you mean exactly. Sometimes they're used to prove some logical proposition directly, but they're not used as a complete software verification tool, because they're rather limited on their own. [1]: When applied to the code directly. We have ways of scaling formal methods by verifying high level specifications.