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.

Continue reading Download file Download abstract about Using State Diagrams for Understanding Correctness in Concurrent Programming