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.

WS 2015: Testing with Symbolic Execution

  • V3Ü2, ECTS: 6
  • Lecturer: Prof. Dr. Klaus Wehrle
  • Assistants: Daniel Schemmel, Oscar Soria Dustmann
  • Study Course: Master Informatik (Software und Kommunikation), Master Software Systems Engineering (Communication), Master Media Informatics
  • See also: Campus
  • Dates:
    • Kick-off Meeting: 2nd of November at 13:00 (2015-11-02T13:00:00).
    • The remaining dates will be determined later on.

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.

Prerequisites

This class will serve as an introduction on how to conduct research in communication systems. Besides learning about the actual topics, taking this course is an ideal preparation for doing a master thesis in our group. The course is only open for Master students. You should have prior knowledge at least in the basics of data communication and an interest in doing independent research. As this course is supposed to be highly interactive, seats are limited. Should we receive more registrations than seats available, we may select students FCFS.