3 ms·

can check most properties expressible in TLA+ Lamport's TLA contains ZF set theory. That makes TLA super expressive. Unless a major breakthrough has happe

• pron 7y ago
  > What is the most complex property that has been established in TLA fully automatically with no hand tweaking etc for more than 50,000 LoCs? And how does that complexity compare to for example the complexity of the formula that has been used in the verification of SeL4? TLC, a model checker for TLA+, is commonly used to verify arbitrary properties -- at least as "deep" as those used in seL4, and often deeper -- of TLA+ specifications of a few thousand lines. Those properties can informally correspond to codebases with hundreds of thousands of lines, but there is currently no method for formally verifying arbitrary properties of 50KLOC, be it automatic or manual. Automated methods, however, are used either for deep properties (quantifier alterations) of few k-lines of spec/code or shallower (though still non-local and non-compositional) properties of 50-100KLOC. Manual deductive methods are virtually used for nothing outside of research projects/teams, except for local, compositional properties, of the kind expressible by simple type systems. I clarified further here: https://news.ycombinator.com/item?id=22146186 https://news.ycombinator.com/item?id=22146186 > So first-order logic is not deductive, because it doesn't yield a direct proof of FALSE? In any logic you can work deductively in the proof theory, or in the model theory. DPLL SAT solvers work in the model theory of first-order logic. Also, SAT solvers work on propositional logic, not first-order logic. Because of completeness, we know that every model-theoretic proof corresponds to a proof-theoretic proof, but that's not how most SAT algorithms work (except for resolution solvers). > There is an interesting question here: what is the precise meaning of "deductive"? It means using the syntactic inference rules of a proof theory, rather than the semantic rules of a model theory (possibly relying on completeness meta-theorems, as in the case of propositional logic, although that's not relevant for most interesting first-order theories). SMT solvers employ SAT, and can work on some first-order theories. I am not familiar with all the techniques SMT solvers use, but I believe they employ both proof-theoretic and model-theoretic techniques. In any event, as I mentioned before, SMT solvers are rarely used alone, because they're very limited. They are used as automated helpers for specific steps in proof assistants (TLAPS, the TLA+ proof assistant makes heavy use of SMT solvers for proof steps), for local properties of code (e.g. OpenJML for Java, in Dafny and in SPARK) or as components in CEGAR model checkers and in concolic test systems.
  • Cladode 7y ago
    TLC ... is commonly used to ... at least as "deep" as those used in seL4, and often deeper What you are in essence implying here is that the SeL4 verification can be handled fully automatically by TLC. I do not believe that without a demonstration ... and please don't forget to collect your Turing Award! One problem with model-checking is that you handle loops by replacing loops with approximations (unrolling the loop a few times) and in effect only verifying properties that are not affected by such approximations. In other words extremely shallow properties. (You may use different words, like "timeout" or "unsound technique" but from a logical POV, it's all the same ...) the model theory ... rather than the semantic rules of a model theory All mathematics is deductive. ZFC is a deductive theory, HOL is a deductive theory, HoTT is a deductive theory. MLTT is a deductive theory, Quine's NF is a deductive theory. With that, what mathematicians call a model is but another deductive theory, e.g. the model theory of Peano Arithmetic happens in ZFC, another deductive theory. The deductive/non-deductive distinction is really a discussion of different kinds of algorithms. Deduction somehow involves building up proof trees from axioms and rules, using unification. It could be fair to say that concrete DPLL implementations (as opposed to textbook presentations) that are based on model enumeration, non-chronological backtracking, random restarts, clause learning, watched literals etc don't quite fit this algorithmic pattern. I am not sure exactly how to delineate deductive from non-deductive algorithms, that's why I think it's an interesting question. SMT solvers are rarely used alone, I agree, but model checkers, type checkers for dependent types , modern testing technques, and (interactive) provers all tend to off-load at least parts of their work to SAT/SMT solvers which makes the opposition between deductive and non-deductive methods unclear. * * * BTW I am not arguing against fuzzing, concolic, model checking testing etc. All I'm saying is that they too have scalability limits, just that the scale involved here is not lines of code.
    • pron 7y ago
      > What you are in essence implying here is that the SeL4 verification can be handled fully automatically by TLC. No, I am not. Read what I wrote again :) > and please don't forget to collect your Turing Award! Some people have already beat me to it. The 2007 Turing Award was awarded for the invention of model checkers that precisely and soundly check deep properties. > One problem with model-checking is that you handle loops by replacing loops with approximations No, that's what sound static analysis with abstract interpretation does. Model checkers are both sound and precise, i.e. they have neither false positives nor false negatives. To the extent they use sound abstraction (i.e. over-approximation), as in CEGAR algorithms, they do so to increase performance and to sometimes be able to handle infinite state spaces. A model checker, however, is always sound and precise, or else it's not a model checker. > In other words extremely shallow properties. Model checkers commonly check arbitrarily deep properties. Engineers in industry use them for this purpose every day. > All mathematics is deductive. Yes, and all (or much, depending on your favorite philosophy of mathematics) of it has models. If you have two apples in one hand and one apple in the other and you count how many you have, you have not done so using deduction in any logical theory. That had you used such a process you would have also reached the same result is because of soundness and completeness meta-theorems. That mathematics has both proof and model theories, and that they're compatible, is the most important result in formal logic. > All I'm saying is that they too have scalability limits, just that the scale involved here is not lines of code. All verification methods are limited by both size of code and depth of properties. For non-trivial property, the least scalable method, on average, is deductive proof. Which is not to say it is not useful when automated methods have failed.