Abstract: In this talk, I will present the results of model checking the NASA robot controller system. The verification has been conducted in the integrated design and verification framework that has been implemented by the combined efforts of the model checking groups at the University of Texas at Austin and Bell Laboratories. I will discuss how the combination of the previously existing and newly developed state space reduction techniques used in the integrated framework enables the practical verification of large-scale software systems. In the conclusion, I will outline a number of research directions that I believe might lead to the improvements of software model checking.