4 ms·

You're not wrong when it comes to the theoretical, general case. However, you shouldn't forget that in practice, we're not interested in every possible problem

• pron 9y ago
  > A weaker model often allows for better heuristics. Do you have any evidence for that? I have not seen this claim made anywhere. The reason is that heuristics apply in cases where the problem at hand can be stated in terms of a lower-complexity problem, and that happens regardless of model. Is there empirical data showing this is happens more often in restricted models? Intuitively, I see no reason why it should. > Take SAT solvers, for example. SAT is NP-complete, which is (well, we don't know for sure, but that's the working hypothesis) much easier than even verification of FSMs (PSPACE-complete). We don't have any similar working heuristics for, say, TQBF (PSPACE-complete), and even SAT solvers fail often. > yet the best heuristic to determine whether the C program outputs 1 for any of its possible inputs, might be to run it once for each input combination (which would take longer than the age of the universe for even 10k variables). Most autoamtic software verification doesn't work like that at all, but through a process called abstract interpretation which can conservatively project the problem onto a much smaller state space (that is basically one way to look at how type systems work). The beauty of SAT solvers is that they require no such semantic approximations, and appear to work on arbitrarily difficult problems (except when they don't). So far, they work by magic -- we don't know why they're so effective in practice. But the hope of finding such a general algorithm that happens to work on many real-world instances of problems that are at least PSPACE- or 2EXP-hard problems are not great. It all comes down to studying special cases, and I don't see a particularly good reason (and I haven't encountered any research to that effect) for how to make such "good" instances more likely using some restricted language.
  • adwn 9y ago
    > Is there empirical data showing this is happens more often in restricted models? Are you asking for studies? How would you even rigorously define the hypothesis? > SAT is NP-complete, which is [...] much easier than even verification of FSMs (PSPACE-complete). So? How does that invalidate my example? > The beauty of SAT solvers is that they require no such semantic approximations, and appear to work on arbitrarily difficult problems (except when they don't). So far, they work by magic -- we don't know why they're so effective in practice. But that's the point! For real-world problem instances, you'll find that automatically SAT solving a CNF model works much better than applying an automatic theorem prover to the C program that generated the CNF model. That's because in practice, it's easier to design heuristics that work on a propositional formula than it is to design heuristics that work on CNF-generating C programs. If that were not true, then we wouldn't need SAT solver – we'd just run the automatic theorem provers on the C programs that generate the CNF model. > I don't see a particularly good reason (and I haven't encountered any research to that effect) for how to make such "good" instances more likely using some restricted language. And yet it works extremely well in the case of the CNF-generating program vs. SAT solving the generated CNF model. That is a pretty strong argument, you cannot just dismiss it because PSPACE harder then NP.
    • pron 9y ago
      > Are you asking for studies? How would you even rigorously define the hypothesis? Preferably studies, but even intuition would do at this point. You don't need to rigorously define the hypothesis, just demonstrate which kinds of patterns susceptible to commonly applied automated reasoning occur more frequently when the same application is written in a TC or non-TC language. The thing is that it's often easy to recognize special cases even in TC languages (e.g., deducing that a function is total in a TC language is easy in those cases where the function resembles those used in non-TC languages). I'm not saying languages can't make verification easier. For example, recognizing a terminating loop may be a bit easier in a language with `for` loops than in a language that only has a `goto` construct, and a language with less/no aliasing makes local reasoning much easier; I'm saying that that help does not stem from restricting the computational model (just as removing `goto` does not reduce the computational power). Turing-completeness in itself is a red herring when it comes to the question of how languages can help verification. But I don't understand even the general line of your argument. Even supposing that SATing a CNF formula automatically generated from C is easier than other approaches (it isn't), this does not show that writing CNF directly is more advantageous than writing C. After all, a simple mechanical translation exists, so why should I write CNF formulas if writing equivalent C code is easier? > you'll find that automatically SAT solving a CNF model works much better than applying an automatic theorem prover to the C program that generated the CNF model. It doesn't, though. Many automatic problems are easier to verify using abstract interpretation than SMT. > So? How does that invalidate my example? That a magical 50-year-old algorithm that no one understands to this day happens to exist for the very simplest of intractable problems does not mean that we can hope for similar success for much, much harder problems. When it comes to program verification, SAT (used in SMT) is effective only in a very controlled and limited way (I know because I use formal verification). No one believes SMT solvers could be extended to verify full programs.