An educational software system of a tiny self-compiling C compiler, a tiny self-executing RISC-V emulator, and a tiny self-hosting RISC-V hypervisor.

Turn a RISC-V binary into a bit-precise BTOR2 model and let a model checker hunt bugs across every possible input - in ~0.1 s where the reference takes 139 s. Includes a browser-based witness visualizer and symbolic command-line arguments (working; design still being rethought). Equivalence with selfie's rotor: 36/36 paired verdicts.

This is the homepage of the Computer Science for All courses by Professor Christoph Kirsch at the University of Salzburg, Austria.

Introduction to Compiler Construction 2016

Systems Engineering 2015

Advanced Operating Systems 2015

Introduction to Operating Systems 2015

Concurrency and Memory Management Seminar 2015

Introduction to Compiler Construction 2015

Systems Engineering 2014