5 ms·

SPIN and TLA+ aren't proof assistants at all - they're model checkers, that is, they simulate a model some number of times and check that the desired properties

SPIN and TLA+ aren't proof assistants at all - they're model checkers, that is, they simulate a model some number of times and check that the desired properties hold in all explored states. Obviously this means they're not providing a guarantee that the properties hold for all states: there's no proof, only evidence. This doesn't mean they're useless, but it does mean they're not proof assistants. ACL2 is a proof assistant, at least, but it's not based in type theory, so that's probably why they didn't use or improve it. ACL2 looks like it's specifically intended to aid in proving theorems about models of software systems, as well, which probably makes its logic system a bit clunky to use when expressing theorems about mathematical structures.

nickpsecurity 8y ago
I meant most successful uses of verification tech, not proof, for SPIN. I shoudve worded that better. There is a version of it in a proof assistant called Favela if I recall. TLA+ has a proof system (TLAPS) and a model checker. Finally, if state and transitions are small, then a model-checker can give you similar assurance as a proof by essentially checking everything. These days, that's rarely the case, though. ACL2 was designed for real hardware and software. That's what many use it for. Rockwell-Collins builds CPU's, separation kernels, and low-level software for NSA with it. I agree author maybe dodged cuz it's not type theory.
avodonosov 8y ago
Model checking is a proof method. If all possible states are explored, that is a pfoof (Proof by exhaustion).
- pron 8y ago
  It's not exactly proof by exhaustion, as model checkers don't actually check all assignments, even explicit-state model checkers (because even in finite state cases, verified propositions are about infinite behaviors; you often model-check propositions much more elaborate than "X never happens in any state"), and algorithms like DPLL for SAT model-checking don't even do explicit state visits. Rather, it is a proof in the model theory of the logic.
pron 8y ago
1. TLA+ is a language. TLA+ specifications can be verified with either a model checker or a proof assistant. TLA+'s proof language is one of the most elegant I've seen. 2. A model checker most certainly provides 100% guarantees. This is why it's called a model-checker: it checks that a system's Kripke structure is a model[1] (i.e. a satisfying assignment) for a formula. It's just that model checkers often fail to check infinite state spaces and so people often check a finite instance of a specification. While model checkers have occasionally found errors in (informal but peer-reviewed) "proofs", I am not aware of any cases to the converse (obviously, when a finite instance was used for an infinite-state system). Both model checkers and deductive proofs have limitations and are generally complementary, but currently model checkers are considered to be much more scalable. Also, model checkers don't "simulate a model some number of times." (the model-checking algorithm for temporal logic won the Turing award for its inventors). Even in finite state cases, model checkers check temporal formulas on infinite behaviors (e.g. that every request is eventually matched by a response). [1]: https://en.wikipedia.org/wiki/Model_theory https://en.wikipedia.org/wiki/Model_theory
- grumdan 8y ago
  Some model checkers are bounded model checkers, for example CBMC, a bounded model checker for C. In practice this sometimes means they only unroll loops a certain number of times, so they might miss assertion violations occurring in later iterations of a loop. You're right though that there are model checkers that are not bounded and these do provide guarantees.
  - pron 8y ago
    Yes, as their name suggests, bounded model checkers check bounded models rather than models. In the literature, bounded models are virtually never mentioned unqualified (i.e., a bounded model checking algorithm won't be presented as a model checking algorithm).

nickpsecurity 8y ago

I meant most successful uses of verification tech, not proof, for SPIN. I shoudve worded that better. There is a version of it in a proof assistant called Favela if I recall. TLA+ has a proof system (TLAPS) and a model checker. Finally, if state and transitions are small, then a model-checker can give you similar assurance as a proof by essentially checking everything. These days, that's rarely the case, though. ACL2 was designed for real hardware and software. That's what many use it for. Rockwell-Collins builds CPU's, separation kernels, and low-level software for NSA with it. I agree author maybe dodged cuz it's not type theory.

avodonosov 8y ago

Model checking is a proof method. If all possible states are explored, that is a pfoof (Proof by exhaustion).

pron 8y ago
It's not exactly proof by exhaustion, as model checkers don't actually check all assignments, even explicit-state model checkers (because even in finite state cases, verified propositions are about infinite behaviors; you often model-check propositions much more elaborate than "X never happens in any state"), and algorithms like DPLL for SAT model-checking don't even do explicit state visits. Rather, it is a proof in the model theory of the logic.

pron 8y ago

1. TLA+ is a language. TLA+ specifications can be verified with either a model checker or a proof assistant. TLA+'s proof language is one of the most elegant I've seen. 2. A model checker most certainly provides 100% guarantees. This is why it's called a model-checker: it checks that a system's Kripke structure is a model[1] (i.e. a satisfying assignment) for a formula. It's just that model checkers often fail to check infinite state spaces and so people often check a finite instance of a specification. While model checkers have occasionally found errors in (informal but peer-reviewed) "proofs", I am not aware of any cases to the converse (obviously, when a finite instance was used for an infinite-state system). Both model checkers and deductive proofs have limitations and are generally complementary, but currently model checkers are considered to be much more scalable. Also, model checkers don't "simulate a model some number of times." (the model-checking algorithm for temporal logic won the Turing award for its inventors). Even in finite state cases, model checkers check temporal formulas on infinite behaviors (e.g. that every request is eventually matched by a response). [1]: https://en.wikipedia.org/wiki/Model_theory https://en.wikipedia.org/wiki/Model_theory

grumdan 8y ago
Some model checkers are bounded model checkers, for example CBMC, a bounded model checker for C. In practice this sometimes means they only unroll loops a certain number of times, so they might miss assertion violations occurring in later iterations of a loop. You're right though that there are model checkers that are not bounded and these do provide guarantees.
- pron 8y ago
  Yes, as their name suggests, bounded model checkers check bounded models rather than models. In the literature, bounded models are virtually never mentioned unqualified (i.e., a bounded model checking algorithm won't be presented as a model checking algorithm).