Formal Methods Teaching: Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings

This tutorial presents PSEUCO [1], an academic programming language designed to teach concurrent programming. The language features a heavily simplified Java-like look and feel. It supports shared-memory as well as message-passing concurrent programming primitives. The behaviour of PSEUCO programs is described by a formal semantics mapping on value-passing CCS or coloured Petri nets [2], and is made executable using compilation to Java. PSEUCO is not only a language but an interactive experience: PSEUCO.COM [1] provides access to a web application designed for first hands-on experiences with CCS and with concurrent programming patterns, supported by a rich and growing toolset. It provides an environment for students to experiment with and understand the mechanics of the fundamental building blocks of concurrency theory and concurrent programming based on a complete model of the program behaviour. PSEUCO and PSEUCO.COM constitute the centerpiece of an award-winning lecture series, mandatory for Bachelor students at Saarland Informatics Campus. Acknowledgments. This work was partially supported by the ERC Advanced Investigators Grant 695614 (POWVER) and by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 389792660 – TRR 248 (see https://perspicuouscomputing.science).