4 ms·

> Because that would make the verification problem even harder (possibly to the point of undecidability). And this approach simply doesn't make sense. What? If

> Because that would make the verification problem even harder (possibly to the point of undecidability). And this approach simply doesn't make sense. What? If foo terminates and bar terminates, than foo bar clearly terminates. How does this make no sense? > Most correctness properties are just not compositional (inductive), and the belief that a non-compositional property can be proven by combining results about the components at a cost that scales with their number (polynomially, exponentially -- take your pick) is mathematically false. Ok, let's check your blog and what paper you mention > A Parametric Analysis of the State-Explosion Problem in Model Checking⋆ What? You state that proving doesn't scale referring to constraint based solutions? Sure, they don't scale. What this foobar example has to do with this tho? Foo does not terminate due to exception, and so does Foo Bar. How doesn't this compose? > I don't understand this simple proof. How does allowing some automation prove that it's not the method least amenable to automation? Because you can automate anything you can prove with a SMT or model checker?

pron 7y ago
> 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.

pron 7y ago

> 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.