WG211/M11Herrmann

I will present a new aspect of software engineering which involves the automatic derivation of program properties during generation of low-level programs (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. I am convinced that efforts are better spent in developing analyses together with the program generation or interactively with the manual design process. The predominant development approach in practice is to first write a program and then to profile 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 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 unite both a rapid program development and an analysis which benefits from design knowledge and can provide results which are parameterised, i.e. valid for an entire range of control parameters.