3 ms·
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 certa
by 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 agoYes, 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).