Area

Master
Software Technology lives at the core of computer science, and no other specialization area can do entirely without it: in the end the goal of all computer scientists is to produce executable code. Everyone producing software has to answer questions as to how to write software, what other software to use, what tools to use, how to interface with other products, how to specify, verify and test, how to document and how to plan the production process. The ST master program focuses on the following themes: programming methods, programming language design and implementation, software engineering tools, program analysis and program transformation, specification and verification techniques. We strongly believe that theory development, tool construction and application of the tools go hand in hand and are dedicated to integrate all three aspects in all the subjects we study and teach.

----++ Generic Programming and Type Systems

Over the years programming languages have become more and more expressive; we no longer only abstract over statements (procedures) and expressions (functions), but also over types. Recent developments enable us to talk about type indexed functions, kind indexed types etc. This increased expressiveness enables us to write less code, and to reuse the code written in a much more flexible way. Class systems enable us furthermore to abstract over whole collections of design decisions. An additional effect of the use of more general and expressive type systems is that they also provide an implicit correctness proof of the program; as a result far less debugging and testing remains. With the increasing use of XML for encoding all kind of data to be stored and exchanged the ability to handle such data in a generic ways becomes of essential importance. Students learn about generic programming techniques, type analysis, and the application of such techniques in XML based programming, for example in the construction of generic editors.

-----++ Programming Language Implementation

As programming languages become more and more expressive their ease of use for the every day user unfortunately does not increase; thus a subset, a special library or even a special purpose language is defined for a specific application area. General programming languages are more and more used as powerful tool sets to support the use of such special purpose formalisms in an efficient way. Polymorphic types and lazy evaluation make it easy to define so-called combinator languages that enable the embedding of a special purpose language into a general purpose language. Such combinator languages support fast and easy construction of programs wherever possible, while maintaining full expressiveness to be used wherever needed. We study the construction of combinator libraries, how to embed global analyses in the implementation, and how type systems help us to define such languages. Special interest is paid to generic implementation techniques that enable us to present error messages stemming from the inner working of the implementation in terms of the special purpose constructor language.

----++ Programming Methodology

An actual piece of code is the result of many, mostly independent, design decisions that each deal with a different aspect of the specification. Unfortunately the results of such decisions (sometimes expressed in the form of "design patterns") are dispersed all over the program text, and consequently hard to change or undo. The recognition that this is happening over and over again has resulted in the research area coined "aspect oriented programming". Especially in the area of object-oriented programming, with its less well developed abstraction mechanism, the need for such an aspect oriented view towards a product is increasingly important. We study the deficiencies of current programming formalisms, and seek to extend them with support for first- class aspects that can be passed as argument and can be abstracted from.

----++ Program Transformation

One way of implementing a program is not by applying a one-step compilation, but by gradually transforming a high-level, but probably inefficient specification into a low-level, but highly efficient implementation. We apply this approach for example in the generation of machine code for digital signal processors. Another area where program transformation is important is in dealing with legacy code: it is in many cases simply not feasible to throw away existing code. We may however try to analyse such code in order to recover parts of its original specification hidden in the outcome of many implementation decisions made in the past, and then transform the program into its new, currently desired form based on the result of such analyses. The group has extensive experience in the design, implementation and use of programming transformation systems.

----++ Program Correctness

The holy grail of programming is the construction of code that is guaranteed to function correctly. Normally one tries to achieve this goal by debugging and systematic testing. When dealing with distributed algorithms this is unfortunately no longer possible. A rigorous approach, based on formally defined semantics and specification mechanisms is needed to prove distributed algorithms correct. Even after an algorithm has been proven correct it is not yet guaranteed that the final implementation was made according to the idealized case that was proved correct, whereas on the other hand the formal verification of the final product is far out of reach. We construct environments in which the formal verification and the incorporation of the verified code into a product are integrated; as such this area of research is strongly linked with the areas described above. 

----++ Program Analysis

To be able to perform program transformation, information must be obtained from source code
efficiently. This is the area, which includes most notably the area of type inferencing and
checking. Other examples of program analysis are dead-code analysis, security analysis,
live variable analysis, control-flow analysis, strictness analysis and binding time analysis.