Trustworthy Computer Systems

•  Software Verification 
  The goal of software verification is to mathematically assure that a given program fully satisfies all its expected requirements. In order to improve the quality of their final products, many major companies include software verification along with testing in their software production process to increase the quality of their final products.
• Program Synthesis 
  Program synthesis is the task of constructing a program from user intent expressed in high-level descriptions. The user intent can be in various forms, e.g., examples, formal requirements, resource constraints or a combination of different formats. With the increased number of people who have access to computers on a daily basis and given the fact that many of them are not programmers, the goal of synthesis is to generate programs using simpler forms of inputs from the user.
  
• Software defined networking 
  Software Defined Networking (SDN) is an emerging network architecture that separates the control logic of the network (control-plane) from the underlying switches (data-plane). SDN promotes logical centralization of network control and introduces network programmability. The research in this area is about to design high-level programming languages for networks and to introduce new approaches to synthesize/verify the programs.
  
• Model-based testing 
  Testing and debugging are major parts of software development and together account for more than half of the total development cost. Model-based testing is a structured method that brings rogour to testing by using models that steer the test-case generation and execution process. We research model-based testing techniques both from theoretical and empirical perspectives.
•  Software product lines 
  Variability is an inherent part of many software systems and software product lines provide a near paradigm to address variability as a first-class citizen in the development process. Our research in software product lines addresses variability-aware models, model learning techniques, and testing techniques.
•  Cyber physical systems 
  Cyber-physical systems are the result of the tight integration of computer systems with their physical environment and communication networks. This leads to a very rich domain that combines discrete algorithms with continuous dynamics and stochastic behaviour of networks. We research logical foundations of cyber-physical techniques as well as rigorous model-based testing techniques for such systems.

Reading Group Page>>