4 ms·

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

by 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.
- adwn 9y ago
  > but even intuition would do at this point. Maybe this example helps: I should be easier to write analysis heuristics for a language that only allows loops of the form "for i = 1...n" than for one which also has while-loops, gotos, and unrestricted C-style loops. Maybe not from a theoretical point of view – after all, both languages are equally Turing-complete – but from a practical one, since there are more language constructs that have to be covered by the analysis. Sure, you can mechanically translate all loops from the second language to "for i = 1...n" loops, but that transformation is not trivial and has to be implemented first. > 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? My point isn't that we should hand-write CNF formulas. What I'm saying is, that automatically solving CNF formulas is easier than automatically solving a C program that expresses the same thing. Example: a Sudoku solver. Given a partially filled 9x9 matrix, * ) Program 1 takes as input an assignment for the unfilled fields (free variables). It outputs yes/no indicating whether the input satisfies the Sudoku rules. * ) Program 2 generates a CNF instance which encodes the Sudoku rules and the partially filled matrix. The variables represent the unfilled fields. Program 1 and the output of program 2 are equivalent in the sense that they encode the same problem instance, but the CNF generated by program 2 is in a much more restricted language than program 1. You can write a decent (although not state-of-the-art) CNF parser and SAT solver in a few 100 lines of code, but you will be hard-pressed to write even the parser for a general C program in that space, let alone something that can understand C's semantics, an automatic solver using abstract interpretation, and some heuristics to speed things up (only those heuristics are allowed to be somewhat tailored to this type of problem, everything else has to be general-purpose – just like the SAT solver, which is general purpose and has a few heuristics that speed up many practical instances).
  - pron 9y ago
    > It should be easier to write analysis heuristics for a language that Quite possibly, and that's exactly what I said. Languages may assist formal reasoning (although how is not always clear[1] and your example may or may not be valid -- the transformation in the well-behaved cases may be quite easy; compilers and static analyzers do such analysis all the time), but that's not due to a weakening of the computational model. > What I'm saying is, that automatically solving CNF formulas is easier than automatically solving a C program that expresses the same thing. Right, but as the transformation is mechanical, there is no reason to prefer one language over the other. They're equivalent -- in this particular scenario -- from both a theoretical and a practical point of view. Static analyzers commonly perform transformations -- from the programming language to SMT-LIB and/or using abstract interpretation. > but you will be hard-pressed to write even the parser for a general C program in that space Writing a compiler for Pascal is much harder than writing an assembler. That's not an argument for writing assembly by hand over writing Pascal. [1]: One example is a pure-functional language like Haskell vs. an imperative one like Java. Well-behaved Haskell allows for equational reasoning while Java "only" allows for assertional reasoning, but the common use of higher-order functions makes some automatic reasoning methods much harder than the familiar and powerful assertional reasoning approaches.

by adwn 9y ago

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.

adwn 9y ago
> but even intuition would do at this point. Maybe this example helps: I should be easier to write analysis heuristics for a language that only allows loops of the form "for i = 1...n" than for one which also has while-loops, gotos, and unrestricted C-style loops. Maybe not from a theoretical point of view – after all, both languages are equally Turing-complete – but from a practical one, since there are more language constructs that have to be covered by the analysis. Sure, you can mechanically translate all loops from the second language to "for i = 1...n" loops, but that transformation is not trivial and has to be implemented first. > 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? My point isn't that we should hand-write CNF formulas. What I'm saying is, that automatically solving CNF formulas is easier than automatically solving a C program that expresses the same thing. Example: a Sudoku solver. Given a partially filled 9x9 matrix, * ) Program 1 takes as input an assignment for the unfilled fields (free variables). It outputs yes/no indicating whether the input satisfies the Sudoku rules. * ) Program 2 generates a CNF instance which encodes the Sudoku rules and the partially filled matrix. The variables represent the unfilled fields. Program 1 and the output of program 2 are equivalent in the sense that they encode the same problem instance, but the CNF generated by program 2 is in a much more restricted language than program 1. You can write a decent (although not state-of-the-art) CNF parser and SAT solver in a few 100 lines of code, but you will be hard-pressed to write even the parser for a general C program in that space, let alone something that can understand C's semantics, an automatic solver using abstract interpretation, and some heuristics to speed things up (only those heuristics are allowed to be somewhat tailored to this type of problem, everything else has to be general-purpose – just like the SAT solver, which is general purpose and has a few heuristics that speed up many practical instances).
- pron 9y ago
  > It should be easier to write analysis heuristics for a language that Quite possibly, and that's exactly what I said. Languages may assist formal reasoning (although how is not always clear[1] and your example may or may not be valid -- the transformation in the well-behaved cases may be quite easy; compilers and static analyzers do such analysis all the time), but that's not due to a weakening of the computational model. > What I'm saying is, that automatically solving CNF formulas is easier than automatically solving a C program that expresses the same thing. Right, but as the transformation is mechanical, there is no reason to prefer one language over the other. They're equivalent -- in this particular scenario -- from both a theoretical and a practical point of view. Static analyzers commonly perform transformations -- from the programming language to SMT-LIB and/or using abstract interpretation. > but you will be hard-pressed to write even the parser for a general C program in that space Writing a compiler for Pascal is much harder than writing an assembler. That's not an argument for writing assembly by hand over writing Pascal. [1]: One example is a pure-functional language like Haskell vs. an imperative one like Java. Well-behaved Haskell allows for equational reasoning while Java "only" allows for assertional reasoning, but the common use of higher-order functions makes some automatic reasoning methods much harder than the familiar and powerful assertional reasoning approaches.