Teaching with Logika: Conceiving and Constructing Correct Software

Slang is a subset of Scala designed for coding high assurance software. It is supported by a highly automated verification tool called Logika that incorporates multiple forms of formal methods, presented in terms of programming-oriented notations and activities. In this paper, we describe our teaching approach for how to conceive and construct correct software using Slang and Logika. A key feature of our approach includes presenting specification, coding, testing, and verification as an integrated engineering methodology. We further motivate students by illustrating Slang/Logika’s use in broader contexts of model-based development and assurance of critical embedded systems. We describe our experience in using Logika for teaching at both the undergraduate and graduate level. A variety of pedagogical materials are available including the open source Slang/Logika implementation, lecture slides, and course notes.