Research Focus Class

Our Research Focus Classes (RFC) are a special kind of lecture: they are more interactive and research oriented than typical lectures. Students participating in an RFC should be aware that they are not only getting in touch with real research but also have to expect doing independent work.

What is Symbolic Execution?

Symbolic Execution is a rigorous, automated testing approach. It was proposed 30 years ago but has become possible only in recent years due to computation power and memory of modern machines as well as significant advances in SMT solvers (Satisfiability Modulo Theory).

By automatically exploring all or at least most possible execution paths, it is able to not only check the correct behaviour of the most likely cases, but also detect corner-case errors that may otherwise remain undetected for several years or even decades. There are several tools implementing Symbolic Execution (e.g. KLEE, SAGE, Chef, S2E, JPF, ...) to create test-cases for the developer to further analyse.

Contrary to many model based approaches, SE actually analyses real code, like C projects and has been and is being used to verify e.g. Linux Coreutils, parts of the Windows operating system and OpenFlow applications.

Structure of the Research Focus Class

The RFCs are research-oriented courses following an interactive schema. To do so, we give a short introductory lecture about the topic (5 lecture slots). Afterwards in the concept phase, each participant identifies a research project he/she finds interesting (if necessary, we will help you with this) and prepares a short presentation on this idea. In the remainder of the class you then should do own research on your topic, which, depending on the topic, could consist of experiments, prototypes, analyses, .... Finally, you present your results to the other participants and the COMSYS group.