Correctness and performance are two of the most fundamental concerns in software development. In particular, the increasing complexity of modern computing environment has made it extremely difficult for software applications to be both correct and efficient. Software programs are frequently found to be flawed, and existing technology has fallen behind in providing the necessary programming language and tool support to ensure high quality software development. This research develops programming language as well as compiler analysis and optimization techniques to support the automated translation of software from high-level design to low-level efficient implementations.
This research develops a multilayer code synthesis framework that systematically produces high-quality software by effectively combining software verification techniques with program analysis and compiler optimization in a three-phase translation process. First, starting from the software design phase, the framework automatically translates formal software semantic specifications into object-oriented or procedural implementations based on strategies selected by programmers. Then, based on knowledge from the software-design phase, a sequence of domain-specific optimizations is applied to the implementation to improve algorithm efficiency. Finally, architecture-specific optimizations are applied to performance-critical routines, and the optimized routines are empirically tuned as the application is ported to different machines. Different design and programming languages may be used in each translation phase, and software verification technology will be used to ensure the correctness of each translation. The research focuses on scientific computing and system software applications, where both correctness and performance are of critical concern. The integrated research is expected to significantly improve both the trustworthiness and performance of existing software development.
