Talk "Teaching Formal Methods to Undergraduate Students Using Maude: Why?, How?, and Experiences"

by Peter Ölveczky

Sat, 14 June 2025 at 03:05 pm in Glasgow, Scotland

Abstract: I have been teaching an introductory formal methods course based on Maude—first to third- and fourth-year students, and lately to second-year students—at the University of Oslo for a number of years. The first part of the course introduces functional modules in Maude and covers basic topics in term rewriting, whereas the second part of the course uses Maude to formally model and analyze a number of classic distributed systems, including: transport protocols such as the alternating bit and the sliding windows protocols, the two-phase commit protocol for distributed atomic commitment, distributed algorithms for mutual exclusion and leader election, and authentication protocols. In this talk I briefly survey some work on teaching formal methods, motivate the use of Maude for an introductory formal methods course, outline the course content, and summarize student feedback and my own impressions about the course.