Reflections on teaching formal methods for software development in higher education

Abstract

Despite the increasing attention to formal verification techniques by industry and academia, the programs of Higher Education to this regard still lie behind, and these concepts are not presented to the majority of Computer Science students trained to be future IT specialists. The primary reason is the presumed complexity of the concepts, tools, and formal processes together with a believed moderate interest of employers, which tends to demotivate students. The starting point of any process of change is typically higher education, which should introduce a thoughtful plan of teaching and practice for the students to get acquainted with these techniques. To do so, it is necessary to preliminary identify the obstacles. The user study described in this paper is examining AutoProof tool to identify the complexities attributed to formal methods. We worked with a cohort of master students in Software Engineering at an Information Technology University and monitored and analyzed their performance and feedback on a pedagogical experience. The work presented in this paper extends our previous research on formal methods education by confirming the findings and adding qualitative considerations to quantitative ones.