This is the homepage of the Computer Science for All courses by Professor Christoph Kirsch.
This is an advanced class on systems engineering for masters students in computer science. The goal of the class is to introduce students to ongoing scientific work in systems and prepare them for working on their masters thesis, in systems but not necessarily. The class focuses on advanced topics in the intersection of systems and formal methods, in particular symbolic execution of machine code through SMT and SAT solving.
After taking the class, using systems and formal methods as foundation, students are able to understand the difference between motivation and problem definition, and know what is involved in defining an interesting problem to work on, regardless of any particular motivation, how to work on a problem for which they a-priori do not know a solution, and finally how to give a presentation with proper problem definition, solution, and conclusions.
The class is based on the rotor and bitme toolchain in the selfie system which encodes symbolic execution of RISC-V machine code in logically equivalent SMT and SAT formulae.
Instead of assignments, students are asked to work in teams of 2-3 students on a coding project defined in class. Projects may involve rotor and bitme but do not have to.
The class is organized as part of a series of Computer Science for All classes.