Model checking is emerging as a promising technique for verification of large software systems. The major focus of research in this context is to address the problem of reasoning about infinite-domain variables and to provide helpful, easy-to-understand information for debugging in the event of an error. In this thesis we present the model checker, FocusCheck, for verification and debugging of sequential C programs. FocusCheck (a) constructs and applies on-the-fiy data-abstraction on the push-down representation of programs, (b) identifies Focus-Statement Sequences from the counterexamples which define the context of errors, (c) is able to zoom in on specific program segments that most likely harbor the statements that caused the error, and (d) includes an intuitive graphical user interface which provides the user with various views of the counterexample increasing the readability of the results. We demonstrate the effectiveness of the techniques using a number of case studies. We also propose a heuristic that looks ahead at branch points with the aim to quickly discover a counterexample in fewer steps and less memory.