Iltis: Formal Foundations of Computer Science Online

Spotlight

Extensive Course Material

Iltis is used in introductory courses on logic and theoretical computer science.

Course: Logic for Computer Scientists (German)

Course: Theoretical Computer Science (German)

English courses with slightly fewer exercises:

Course: Logic for Computer Scientists

Course: Theoretical Computer Science

Iltis offers integration into Learning Management Systems (such as Moodle) via the LTI standard

Iltis is also used in university courses on Philosophical logic as well as in a school course on formal languages.

Spotlight

Educational Tasks

A variety of educational tasks in formal foundations of computer science is available in Iltis.

Tasks on Logic

	Propositional Logic	Modal Logic	First-order Logic	CTL
Choosing a vocabulary	✓	✓	✓	✓
Constructing formulas	✓	✓	✓	✓
Transforming formulas	✓	✓	✓	⚙
Demonstrating (un)satisfiability	✓	✓	✓	⚙
Constructing models	✓	✓	✓	⚙
Evaluating formulas	✓	✓	⚙	⚙

Tasks on Formal Languages

Regular Languages

Construction of

regular expressions
deterministic finite automata
non-deterministic finite automata
regular grammars

Specifying words

Specifying Myhill-Nerode classes

Proving inequality of languages

Context-Free Languages

Construction of

push-down automata
deterministic push-down automata
context-free grammars

Specifying words

Specifying derivations in context-free grammars

Proving inequality of languages

Tasks on Computability & Complexity Theory

Computational Reductions

Specifying reductions between graph-based problems, e.g.

Clique ≤ IndependentSet
DirectedHamiltonianCycle ≤ HamiltonianCycle
VertexCover ≤ FeedbackVertexSet
...

Turing Machines

Constructing turing machines ⚙

Simulating turing machines ⚙

General Purpose Tasks

Constructing and manipulating graphs

Constructing proofs via drag & drop ("proof blocks")

Sorting items into buckets (e.g. sorting languages into language classes)

Multiple-Choice questions

⚙: in development

Spotlight

Combining Educational Tasks Into Multi-Step Exercises

Atomic educational tasks can be flexibly composed into multi-step exercises.

Output: vocabulary chosen by student

Used as vocabulary for formulas in a follow-up task

Spotlight

Customizable Feedback Strategies

How much and which feedback is provided to students can be flexibly specified by instructors.

Spotlight

Powered by Research

The development of Iltis is guided by research in CS theory and CS education.

Introduction to Iltis

Teaching Formal Foundations of Computer Science with Iltis M. Schmellenkamp, F. Vehlken, T. Zeume The Education Column (Bulletin of the EATCS 02/24)

Logic

Learning Tree Pattern Transformations D. Neider, L. Sabellek, J. Schmidt, F. Vehlken, T. Zeume
ICDT 2025
arXiv
Discovering and Quantifying Misconceptions in Formal Methods Using Intelligent Tutoring Systems M. Schmellenkamp, A. Latys, T. Zeume SIGCSE 2023
Teaching Logic with Iltis: an Interactive, Web-Based System G. Geck, A. Ljulin, J. Haldimann, J. May, J. Schmidt, M. Schmellenkamp, D. Sonnabend, F. Tschirbs, F. Vehlken, T. Zeume ITiCSE 2019
Introduction to Iltis: an interactive, web-based system for teaching logic G. Geck, A. Ljulin, S. Peter, J. Schmidt, F. Vehlken, T. Zeume
ITiCSE 2018
arXiv

Formal Languages

Detecting and explaining (in)equivalence of context-free grammars M. Schmellenkamp, T. Zeume, S. Argo, S. Kiefer, C. Siems, F. Stebel

arXiv
Exploring Error Types in Formal Languages Among Students of Upper Secondary Education M. Schmellenkamp, D. Stanglmair, T. Michaeli, T. Zeume
Koli Calling 2024
arXiv

Computational Reductions

showcase

Specification and Automatic Verification of Computational Reductions J. Grange, F. Vehlken, N. Vortmeier, T. Zeume
MFCS 2024
arXiv
Tool-Assisted Learning of Computational Reductions T. Kneisel, E. Radtke, M. Schmellenkamp, F. Vehlken, T. Zeume
SIGCSE 2025
arXiv

Spotlight

Active Development

Iltis is under active development and is well on its way to becoming open source.

Iltis is funded by