Teaching formal methods based on rewriting logic and Maude

Abstract

This paper advocates teaching formal methods based on rewriting logic and the Maude tool for the purpose of widening access to formal methods. On the one hand, Maude's elegant, intuitive, and expressive programming/modeling language, its high-performance analysis methods, and some of its academic and industrial applications should make it appealing to a wide range of computer science students. On the other hand, teaching rewriting logic allows us to naturally incorporate substantial formal methods theory, such as equational logic and inductive theorem proving, TRS theory, and model checking. This paper also gives an overview of the content of - and the student feedback to - an introductory formal methods course based on rewriting logic that has been given at the University of Oslo since 2002. © 2009 Springer-Verlag Berlin Heidelberg.