Automatic evaluation of students’ programs is found in both grading and tutoring systems, its aim being the verification of correctness of students’ programs, as well as bugs localization and fixing. The respective evaluation tools should therefore deal with logical programming errors in a way which is comparable to the functionality of modern compilers, which localize syntax errors by highlighting erroneous code, along with delivering messages that help programmers to understand and correct possible syntax errors. As the number of possible program implementation variants, which are correct solutions for a given problem, can be quite large, issues can arise in performing a comprehensive evaluation. Despite the efforts of researchers in this area, the presently known systems do not evaluate students' programs in a satisfactory manner, which requires a new approach to the evaluation of student programs. In this dissertation an approach which combines both program verification with respect to a formal specification and recognition of students' programs based on the semantic distance from a program model is presented. While the former method is implementation independent, thus providing reliable information about program correctness, the latter one precisely localizes bugs and provides minimal corrections which are accommodated to students' intentions. The scientific contribution of the research reported in the dissertation includes program representation through entities, semantic distance of entities, and design of the prototype system implementing the above notions.