WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+

Konstantin Läufer, Gunda Mertin, George K. Thiruvathukal

Background: In this paper, we present our initial efforts to integrate formal methods, with a focus on model-checking specifications written in Temporal Logic of Actions (TLA+), in…