Model Construction: The initial research projects which applied model checking to real source code built models by hand based on relatively small parts of programs (Penix et al. 2000; Havelund, Lowry, and Penix 2001). This was a lot of work. Manual model construction is time consuming and error prone. It is often difficult to get the models right. It requires domain expertise to know what to include and what to leave out.