WG211/M11Herrmann

I will present a new aspect of software engineering which involves the automatic derivation of parameterised program properties during generation of low-level programs (such as assembly code for an abstract machine) from high-level specifications (such as SQL). For certain properties in dedicated application areas, such as worst-case execution time for embedded systems, much effort has been spent to adapt or instrument programs to fit the need of existing analysis tools, but this can only assist such tools concerning aspects they are already prepared for. In industrial settings where manual instrumentation or code adaptation would be infeasible due to the program size, severe limitations such as constant upper bounds on loops are imposed before carrying out a completely automatic worst-case execution time analysis. I think that it could be very useful to derive program properties during the generation including as many design decisions as possible, maybe interactively guided by a manual design process. The predominant development approach in practice is to first write a program and then to test it on concrete data, profile it and change it if it does not fit the expectations. At the other end of the scale is the approach of using a programming language with dependent types, which would provide even strong formal guarantees by an independent instance (the type checker) but also slows down the program development process due to the need to find appropriate proofs at many places. I believe that the approach of combining generation with analysis can establish both a rapid program development and provide an analysis which benefits from design knowledge and delivers results which are parameterised, i.e. valid for an entire range of values for important control parameters, such as the size of the problem instance.