Feature Model Analysis

Feature models are a compact representation of all the products of a software product line in terms of “features”. Feature models are commonly visually represented by means of feature diagrams, and are widely used during development process. The goals of this project will be to represent a feature model programmatically using Satisfiability Modulo Theories (SMT) and enable reasoning.

Software Verification in Practice

Software verification entails the algorithmic analysis of programs to mathematically prove properties of their executions - to prove that given certain assumptions, the code is correct and bug-free. It has found extensive application in embedded, cyber-physical, and safety-critical systems. Among others, it allows verifying array bounds (for absence of buffer overflows), pointer safety, exceptions and user-specified assertions. This project will investigate software engineering aspects of applying verification in practice.

Domain-Specific Language for Transfer Learning / Uncertainty Quantification

Recent breakthroughs in biomedical image analysis have been based on the application of advanced machine learning for large imaging data sets. For instance, convolutional neural network-based classifiers have recently been shown to reach or even exceed human-level performance in a range of disease- and abnormality detection tasks, based on tens of thousands of images. However, such machine learning approaches often fail when confronted with changes to the input data, e.g. images from a different MRI machine, or patients of a different age group or ethnicity.