An Approach to Formal Verification of Programs in Learning C Programming

Learning C programming is very difficult process which requires a large number of skills. Therefore, students often make logical mistakes when solving tasks that require writing program code. Existing approaches allow to check either correctness of program as a whole or syntax correctness only. In this paper, proposed an approach to apply the formal verification method “Model Checking” for detecting logical mistakes at the intermediate steps of the student’s program. We suggest the teacher to build a goal’s tree for each task and then automatically check if that goals achieved by student’s program. We believe that such kind of feedback will help student to understand which actions in the program are performed correctly from the point of view of the task being solved, and which are not. In this paper, discussed the modifications that need to be made to existing formal verification tools to make it helpful in learning C programming. Proposed the plan of experiment which will prove suitability of this approach in learning programming.