WIP: An Engaging Undergraduate Intro to Model Checking in Software
Engineering Using TLA+
WIP: An Engaging Undergraduate Intro to Model Checking in Software
Engineering Using TLA+
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+), into computer science education, targeting undergraduate juniors/seniors and graduate students. Formal methods can play a key role in ensuring correct behavior of safety-critical systems, …