Work summary of Shmuel Schwarz

Computer Science Mentor: Prof. Mordechai Ben-Ari 2006

This thesis describes an investigation into the factors affecting a student’s decision whether to construct a state transition diagram in order to verify the correctness of a concurrent program, or whether to verbally verify the program. I conjectured that...

the advantages of the visual formal tool would cause it to be adopted as a routine part of the students’ practice, but in fact the verbal description was the dominant method of their practice. The reasoning that the students used in choosing a proof method are described. Psychological factors such as personal commitment and evaluation of effort turned out to be more important than the appropriateness of the tool for achieving the goal.