# Formal Methods Education Online: Tips, Tricks & Tools (FOMEO'21)

Satellite workshop of ICALP, July 12, 2021

Online instruction of formal methods has been a challenge in the last year, including teaching of basics of logics and automata theory, formal verification, theorem proving etc. This workshop brings together instructors of formal methods as well as developers of teaching support systems for formal methods to
(a) present web-based teaching support systems for formal methods education, and
(b) discuss tips, tricks & experiences in online instruction gained in the last year.

## Motivation

Our impression is that a lot of nice ideas, tools and tricks for online teaching have been developped, but are not widely known thorugh the community. We would like to know more about what others are doing and strongly suspect that many instructors are very interested in learning about approaches used by others. We, the organizers, are actively involved in building teaching support systems for formal methods. Jan and Maximilian are the current project leads of AutomataTutor, a tool for teaching the foundations of formal languages. Thomas is the project lead of Iltis, a tool for teaching the foundations of logic. In our work, we encountered several other teaching support systems that cover topics of formal methods education, but our impression is that many of these systems are not widely known.

## List of presented tools

Here is a short overview of all the presented tools.

### Logic

• Name: DiMo
Area: logic
Content: editor and solver (satisfiability, validity, equivalence) for parametrized propositional formulas
Usage: by students as support for exercises on discrete modelling in propositional logic; can be used as a sat-solver interface
• Name: Hintikka's World
Area: Modal logic
Content: Examples of Kripke models: muddy children, dining cryptographers problem, etc.
Usage: Explore Kripke models, model checking of formulas
• Name: Iltis
Area: Logics (in the future further fields like formal languages as well)
Content: Exercises for the complete reasoning workflow (modeling, transformation, testing for satisfiability) for propositional, modal, and partially first-order logic; some other tasks like formula evaluation, model construction, ... for these logics; atomic tasks can be combined to form larger workflows
Usage: Iltis can be freely tested under the given link; to use it in your course, please get in touch with us (e.g. via the comment functionality on our website), then you can create your own pages and publish them under a customized link
• Name: Larch
Area: Proof methods for formal logic.
Content: A prototype of an Intelligent Tutoring System that supports learning different proof methods (such as analytic tableaux or sequent calculi).
\$ analytic tableaux method for propositional logic (and more proof methods in the future). The main ideas behind the interface are: step-by-step guidance through the proof, effective hint system and engaging gamification features.
• Name: LogEx, LogAx and LogInd
Area: Logics
Content: (see abstract below)
Usage: (see abstract below)
Area: Logics
Content: (see abstract below)
Usage: (see abstract below)
• Name: Pravda
Area: Proof systems in logic
Content: Exercices in resolution and natural deduction
Usage: Understand proof systems, write proofs
• Name: Sequent Calculus Trainer
Area: logic
Content: constructing formal proofs in sequent calculus with automated feedback on the provability status
Usage: by students as support for exercises on proving validity of formulas in sequent calculus; helps presenting proof construction during lectures
• Name: The Incredible Proof Machine
Area: Logic and formal proves
Content: Game-like exercises in propositional and predicate logic using natural deducation.
Usage: Novel graph-based proof representation with an interactive web- based environment.

### Formal languages and methods

• Name: Automata Tutor
Area: Formal languages
Content: Exercises on DFA, NFA, RE, PDA and CFG (understanding, construction, conversions and further algorithms)
Usage: Register online - Become instructor - Create your own exercises for your course
• Name: pseuCo Book
Area: process calculi, concurrent programming
Content: explanations & interactive exercises on isomorphism, (weak) bisimilarity, observation congruence, and concurrent programming with message passing and shared memory
Usage: contact freiberger@depend.uni-saarland.de for access – you can use the existing exercises in your courses
• Name: pseuCo.com
Area: process calculi, concurrent programming
Content: IDE for CCS & pseuCo (a concurrency-focused programming language with CCS-based semantics)
Usage: immediately usable in your browser – get started here: https://pseuco.com/#/sku/default/tool/landing

### Other

• Name: Tableaunoir
Area: Online blackboard with fridge magnets
Content: Magnets for teaching algorithms, graph theory, games
Usage: Draw, explain, share your board without registration

## Programme on Monday, July 12

We will have short presentations in Zoom sessions, augmented by additional discussions in gather.town, where presenters have their own space to answer questions, discuss and demonstrate in more detail.
All times are given in CEST (Central European Summer Time).

### 10:00-11:00 Formal languages and methods

• Francois Schwarzentruber. Tableaunoir: an online blackboard for teaching formal methods

Tableaunoir is an online collaborative blackboard tool with fridge magnets available in many languages. The main raison d'être of Tableaunoir is the use of fridge magnets, to make interactive animations. The tool provides magnets for teaching algorithms, automata theory and games.

• Maximilian Weininger. Automata Tutor

Computer science class enrollments have rapidly risen in the past decade. With current class sizes, standard approaches to grading and providing personalized feedback are no longer possible and new techniques become both feasible and necessary. Here, we present the third version of Automata Tutor, a tool for helping teachers and students in large courses on automata and formal languages. The second version of Automata Tutor supported automatic grading and feedback for finite-automata constructions and has already been used by thousands of users in dozens of countries. This new version of Automata Tutor supports automated grading and feedback generation for a greatly extended variety of new problems, including problems that ask students to create regular expressions, context-free grammars, pushdown automata and Turing machines corresponding to a given description, and problems about converting between equivalent models - e.g., from regular expressions to nondeterministic finite automata.

• Norbert Hundeshagen and Martin Lange. From Competences to Feedback -- Formal Methods Needed Everywhere

The University of Kassel has traditionally been a stronghold for research in educational sciences and teaching methodologies. The
Theoretical Computer Science / Formal Methods group there is working on the design, development, deployment and evaluation of software
tools for learning support not restricted to areas of theoretical computer science. One of the major aspects of this program is the application of formal methods technology to automatically generate feedback that initiates the users learning process.
In this presentation we will introduce different examples of such feedback systems developed and/or currently in development for the Sequent Calculus Trainer, a tool for learning how to construct formal proofs in propositional/ first-order logic, DIMO, a tool for the support of modelling skills in propositional logic, and the grading of homework exercises on regular languages.
In particular, the feedback systems used in these tools are based on a clear identification of a rather distinct set of competencies, which we believe is beneficial for the applicability of formal methods technology and ultimately for the effectiveness of such learning tools. Furthermore, we will discuss the formal methods applied to address these competencies, their (didactical) limitations, and how the information gathered by this technology can be used to support the learning process by students in particular parts of a course.

• Felix Freiberger, Gregory Stock and Holger Hermanns. Teaching Concurrency Online with pseuCo

In this presentation, we will share our experiences when moving to an online format for the award-winning lecture series Concurrent Programming at Saarland University.
The lecture explains message-passing and shared-memory programming founded in concurrency theory.
We will report how the students made use of our supporting websites and services, including a web application allowing them to develop programs and interactively explore their semantics, a novel website combining book-like explanations and definitions with interactive exercises helping students to practice and learn from live feedback, and a few other bells and whistles.

### 13:00-13:45 Logics: Modelling/Transformations/Reasoning

• Josje Lodder, Bastiaan Heeren and Johan Jeuring. Tools for teaching proofs in logic: LogEx, LogAx and LogInd

To support students practicing with performing proofs in logic, we have developed three systems: LogEx, LogAx and LogInd. LogEx is an Intelligent Tutoring System (ITS) in which a student can practice the rewriting of propositional logic formulae using standard equivalences such as De Morgan's law or distribution. The LogEx domain reasoner cal- culates feedback automatically for propositional logic expressions submitted by students when solving an exercise. For this purpose it uses domain knowledge, such as rewrite steps, common mistakes, and procedures for solving an exercise. LogEx is based on the Ideas framework, which supports the development of ITSs that automatically generate feedback and help for step-wise exercises, for a wide range of problem domains.
The LogEx system supports three different types of exercises: rewriting a formula in disjunctive normal form, in conjunctive normal form, and proving the equivalence of two formulae. Students enter their solution step-wise, providing the next step and the corresponding rule name of the step, and receive feedback after each step. LogEx points out syntax errors, it recognizes a wrongly motivated but correct step, and it provides informative feedback if a common mistake occurs (a so-called buggy rule). An example of the latter might be the distribution of a conjunction over a conjunction. Although the result is an equivalent formula, this application of distribution is incorrect. Our aim is to let the way of working in LogEx resemble solving exercises using pen-and-paper as much as possible. Hence, the equivalence proof component of LogEx facilitates working in two directions. For example, a student can start rewriting the second formula, then switch to the first formula, and go back to the second.
In LogAx [6] a student can practice with performing Hilbert-style proposi- tional logic proofs. LogAx oers the same type of help as LogEx: informative feedback, layered hints, next steps and complete solutions. If suitable, a first hint in LogAx will be a reachable subgoal. LogAx uses a dialog box in which a student chooses the axiom or rule she wants to apply. The actual application of the rule is performed by LogAx. In this way, the student can concentrate on the strategy, and occurrences of syntax mistakes such as missing parentheses are minimized. To give feedback and help, we adapt the algorithm of Bolotov, which gener- ates natural deduction proofs, to Hilbert-style axiomatic proofs. This adaptation can generate a proof for any provable consequence of a set of formulae, and also complete any partial proof.
Our latest tool, LogInd, is a tutoring system for practicing the structural induction proof technique. LogInd guides a student through an inductive proof by explicitly asking to state and prove a base step, an induction hypothesis and the inductive steps.

• Marko Schmellenkamp. Iltis: Teaching Logic in the Web

The Iltis project provides an interactive, web-based system for teaching the foundations of formal methods. It is designed to allow modular addition of educational tasks as well as to provide immediate and comprehensive feedback. Currently, exercises for various aspects of typical automated reasoning workflows for propositional logic, modal logic, and first-order logic are covered.
Recently, Iltis has reached a level of maturity where large parts of introductory logic courses can be supplemented with interactive exercises. Sample interactive course material has been designed and used in such courses with more than 200 students.
We invite all readers to give it a try!
This is joint work with Gaetano Geck, Christine Quenkert, Jonas Schmidt, Felix Tschirbs, Fabian Vehlken, and Thomas Zeume.

• Francois Schwarzentruber. Hintikka's World: teaching epistemic reasoning

Hintikka's World is an online tool for teaching epistemic reasoning. The core idea of Hintikka's World is that epistemic Kripke models are shown as comics. The tool is very graphical. The user can then explore mental states of the agents by clicking on them. The tool contains many classical AI examples, such as the Sally and Anne example. They are all formalized in Dynamic epistemic logic.

### 14:00-14:45 Logics: Deduction

We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic, automated reasoning and formal methods. NaDeA is a browser application for classical first-order logic with constants and functions. The syntax, the semantics and the inductive definition of the natural deduction proof system along with the soundness and completeness proofs are verified in Isabelle/HOL. Finished NaDeA proofs are automatically translated into the corresponding Isabelle-embedded proofs. Hundreds of computer science students have used NaDeA for course exercises and exams since 2015.

• Joachim Breitner. The Incredible Proof Machine

The Incredible Proof Machine is an easy and fun to use program to conduct formal proofs. It employs a novel, intuitive proof representation based on port graphs, which is akin to, but even more natural than, natural deduction.
In this Demo, I'll give a quick intro into the web-based UI, explain some of the features and design decisions, briefly touch upon the meta-theory (which is formalized in Isabelle!), and then I am looking forward to interesting discussion.

• Pierre Le Barbenchon, Sophie Pinchinat and Francois Schwarzentruber. Pravda: a tool for learning formal logic

Pravda is an online proof assistant for learning formal logic (currently natural deduction, Hilbert-style proofs and resolution). Contrary to other tools which are purely graphical, Pravda takes an opposite approach: a proof is just a text. The syntax is very simple: each line is a formula/sequent and the whole proof is thus a sequence of formulas/sequents. Pravda also display tree-form proofs, and proofs can be exported in LaTEX. The tool provides many examples. The tool is easy to extend for capturing other proof systems.

### 14:45-open Discussion and demos in Gather.town

• Jakub Dakowski, Aleksandra Draszewska, Barbara Adamska, Dominika Juszczak, Łukasz Abramowicz and Robert Szymański. Addressing logic students' proof making difficulties with Plugin Oriented Programming and gamification

There have been several attempts at creating Intelligent Tutoring Systems for several proof methods. Nowadays such software usually can give demonstrations and in some cases finish proofs that were already started [1]. Unfortunately, these tools tend to be pretty limited when it comes to customisation options, available proof systems and overall user experience.
This project, called Larch, aims at improving these aspects of ITS. It’s an application designed in hopes of creating a middleman between the researchers trying to implement new hint generation mechanisms and users who usually are unaccustomed to the complicated notation used in formal logic and hard to use interfaces. It guides its users through a chosen proof method, laying out possible options and their consequences, it empowers students to become more proficient, all in a user-friendly way. To achieve that, techniques of gamification were incorporated into the software, along with the best UX practices. Plugin Oriented Programming paradigm was used to create a versatile system, adaptable to users’ needs. The most notable plugins created so far include: an implementation of analytic tableaux for propositional logic, sequent calculi for intuitionistic logic with loop prevention mechanism, and a script for generating TeX code.
Long-term development plans include implementing other plugins as well as measuring the effectiveness of Larch as a tutoring application for students.
[1] Cristiano Galafassi, Fabiane F.P. Galafassi, Eliseo B. Reategui, Rosa M. Vicari, EvoLogic: Intelligent Tutoring System to Teach Logic, Brazilian Conference on Intelligent Systems (Rio Grande, Brazil), (Ricardo Cerri, RonaldoC. Prati, editors), vol. 1, Springer, 2020, pp. 110–121.

• Muhammad Atif. Model Checking through Process Algebra mCRL2

mCRL2 is a formal specification language along with certain tools for formal verification using model checking. Concurrent systems and protocols can be modelled, validated and verified with the toolset. It is available for all widely used platforms from www.mcrl2.org.
Recently, we have developed a GUI which is easy for students and teachers to learn formal verification.

## Registration

Registration for FOMEO'21 is open via the ICALP workshop registration.

The deadline for registration is July 7th AoE. Please feel very welcome to ask any questions via mail to fomeo21@easychair.org!

## Submissions

Deadline: May 8 May 15, 2021

Via Easychair, for more detail see the call