The fundamental problem with model checking, as applied to software, is that it is basically restricted to finite models (so arbitrary precision, for example, is quite problematic). More so, the larger the model (think of it as a search space) the longer checking takes.
Still, finding way to apply model checking to software seems like a very nice research topic.
Posted to SoftwareEng by Ehud Lamm on 3/1/01; 1:39:42 AM

