ABSTRACT. We briefly describe the Logic Workbook project, the culmination of our 5-year long effort to develop a suite of tools aimed at fostering independent active learning in our undergraduate course on first-order logic. It supports students solving sets of problems of multiple kinds (modelling, proving, model building) by integrating our previously stand-alone client-side web apps.

ABSTRACT. In this talk we will present recent efforts on extending the DiMo specification language and the tool's capabilities for providing problem-specific (graphical) output. The tool is already present in FOMEO's list of presented tools.

ABSTRACT. 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. We are now working on integrating Iltis with course management platforms to enable teachers as well as students to monitor their progress. Sample interactive course material has been designed and used in such logic courses with more than 200 students. We invite all readers to give it a try! This is joint work with Gaetano Geck, Marko Schmellenkamp, Jonas Schmidt and Thomas Zeume.

ABSTRACT. Clear, precise and focused communication is one of the key components of education. Formal methods provide a way to achieve all of these goals. Hence, we introduced formal methods in the teaching of the course ``Systems Engineering 1'' as part of the International Master's program of Distributed Systems Engineering (DSE) at TU Dresden in Winter Semester 2019/20. In the same semester, we initiated the concept of ``research-based teaching'' to integrate our research in the teaching by adding exercise on attestation process in the emerging field of confidential computing. In the same semester, teaching was shifted to online format due to COVID19. Altogether in various courses of DSE, there are currently 12 complete exercises (each of 90 minutes) on remote attestation and ProVerif based on the research carried out at the chair. Considerable effort was required to design these exercises, as DSE students typically do not have familiarity with formal methods. To the best of our knowledge (and confirmed by the developers of ProVerif), this is the first initiative to introduce ProVerif to such students.

ABSTRACT. DOMtutor is a set of scripts and problems built for DOMjudge, an evaluation tool used for competitive programming.

ABSTRACT. Tableaunoir was already presented at FOMEO 21. 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. The new feature that will be presented at FOMEO~22 is making slides (presentation).

ABSTRACT. This presentation showcases pseuCo Book, an interactive textbook for concurrent programming, and its use in the \emph{Concurrent Programming} lecture at Saarland University. In contrast to many other tools that have a narrow scope and lack context, or only work as add-ons to textbooks and other course materials, pseuCo Book provides a truly interactive textbook experience where interactive demonstrations and exercises are interwoven with more classical textual elements. PseuCo Book is a work-in-progress and currently has two chapters, one on notions of equality like trace equivalence, bisimilarity, and observation congruence, and one focussing on the fundamentals of practical concurrent programming with message-passing or shared-memory concurrency.

ABSTRACT. The Iltis project provides an interactive, web-based system for teaching the foundations of formal methods. This abstract gives a preview on Iltis' support of exercises on formal languages.

ABSTRACT. Name: Automata Tutor Link: automatatutor.com 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

ABSTRACT. Our research team “Theory of programming”, at the Faculty of Electrical engineering and informatics, Technical University of Košice, Slovakia is interested in theoretical informatics. Our research and teaching are dedicated to formal methods and systems. Currently, we teach the following subjects: Formal languages, Logic for informaticians, Type theory, and Semantics of programming languages. We use traditional (mathematical) methods of teaching using blackboards in a class. The pandemic of Covid 19 has made our teaching complicated. We had to adapt and improvise. We have changed a blackboard in a class to a graphical tablet. But there was still missing a student-teacher interaction when for example a student came after class for a consultation to check if they understand a topic correctly, or if their calculations are correct, and so on. Therefore, we have decided to develop web tools that will simulate calculations as they would be done on a blackboard. The first implemented method is the Structural operational semantics (SOS) over a simple imperative language with the following syntax: • e ::= n | x | e + e | e - e | e * e • b ::= true | false | e = e | e ≤ e | ¬ b | b ∧ b • S ::= x := e | skip | S; S | if b then S else S | while b do S Our tool is developed as a web application, therefore is quickly accessible, with a simple UI. User type a program in our language and a tool will provide a calculation with the following options: • The whole sequence – will display the whole solution in one step. • Step by step – will display the calculations be each configuration of the program’s SOS. Here is also a possibility to interactively guess the next configuration. • Single instruction - provides a simple interface for sliding between configurations. • There are also possibilities for uploading the program from a file, exporting results in a PNG file, showing “help” with the user manual, setting other parameters of UI and input editor (such as color, text size, etc.), and many others.

ABSTRACT. We present LogInd, a tool for teaching structural induction. LogInd supports students in providing inductive proofs of properties of propositional formulae. Students can enter their proofs stepwise and receive feedback on each step. At any moment they can ask for a hint or next step.

ABSTRACT. Prooffold is a tool for displaying structured proofs, in the same spirit than Leslie Lamport's proposition. Prooffold displays a proof in a top-bottom manner: from the general idea of the proof to the technical details. The graphical user interface proposes panels that the user can open/close to see/hide more details. Proofs in Prooffold are written in a dialect of Markdown that offers structural constructions.

ABSTRACT. We present the Sequent Calculus Verifier (SeCaV) and discuss its advantages and disadvantages as a tool for teaching logic, automated reasoning and formal methods. SeCaV is a formalization in the proof assistant Isabelle/HOL of classical first-order logic with constants and functions. The syntax, the semantics and the inductive definition of the sequent calculus proof system along with the soundness and completeness proofs are verified in Isabelle/HOL. SeCaV is accompanied by the SeCaV Unshortener, which is a browser application for developing sequent calculus proofs that are automatically translated into the corresponding Isabelle-embedded proofs. A compact format for the one-sided sequent calculus is used. The system provides feedback on proof rule applications. Online help and examples are available. Hundreds of computer science students have used SeCaV for course exercises and exams. Reference: https://secav.compute.dtu.dk/

ABSTRACT. SIVA is a web application serving for simulation of the tableau algorithm (TA) for the ALC DL. A user builds a completion tree (to prove the input consistency) step by step, supervised by SIVA. The main goal of SIVA is to teach the DL tableau expansion rules and to visualize the completion tree. The visualization with the tool is simpler and more readable than on a blackboard. One of the main advantages is that beside the completion tree also the tableau is visualized.