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 first to write a program and then to analyse 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.