4 ms·

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'

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

by pron 8y ago

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