The goal of the thesis is to conduct a study of the use of Craig's interpolant method in the field of computer system analysis with the focus on the usage of interpolation in verification model checking algorithms. The thesis includes a presentation of the known algorithms in a uniform notation, their comparison in terms of efficiency and applicability to different systems, and well-chosen examples that capture key aspects of each algorithm. The purpose of the examples is also to demonstrate the main differences among the algorithms. The main output of the thesis will be a set of animations that show the execution steps of individual algorithms while illustrating the key ideas of each algorithm in an easily-understandable way.