Project: Programming and Validating Software Restructurings
Legacy software is the result of years of accumulated investment, leading to code bases that are complex, poorly documented, and hard to modify. The maintenance effort for legacy code bases is significant. In fact, maintenance dominates the software development budget over the lifetime of a software system. To keep up the rate of innovation, software engineers should be enabled to make large-scale code restructurings efficiently and systematically to reduce complexity of the code. Modern integrated development environments such as Visual Studio and Eclipse support a fixed set of automated refactoring’s, i.e., transformations that improve the structure of existing code while preserving its behavior. Such refactoring’s are useful, but they are insufficient for the majority of maintenance restructurings, which require the ability to define custom, project specific transformations. Moreover large-scale restructurings do not have to be universally applicable, software engineers should instead be able to validate their correctness in the context of the project under consideration.
The goal of this project is to develop a language parametric framework that supports software engineers to define custom, project-specific software restructurings that can be automatically applied at scale to large code bases, and that supports the validation of the correctness of (the result of) restructurings. We will combine our expertise in language engineering and verification to develop a framework consisting of the following components: (1) A language parametric program model with graph-based semantic models including data-flow, control-flow, and name binding for executing large-scale restructurings of software projects with extraction from and rendering to program texts. (2) A domain-specific language for defining custom restructurings in terms of the concrete syntax of the language under transformation, operating on the semantic program model. (3) Techniques for validating the correctness of (the results of) restructurings, including static checks of safety properties on restructuring specifications, and post-translation validation of structural and behavioral properties of the program after restructuring. We will evaluate the framework by instantiating it to the C++ language, and applying it to restructuring case studies from the C++ code base of Philips.
The project is a collaboration between TU Delft, TU Eindhoven, TNO/ESI, and Philips Healthcare and funded by a project in the NWO/TTW Mastering Complexity (MasCot) program.
The project has funding for three PhD students, two at TU Delft and one at TU Eindhoven.
All PhD students will work two days per week on site at Philips Healthcare in Best to explore software restructuring requirements and test solutions in practice.
TU/e Job Description
The Formal System Analysis (FSA) group at Eindhoven University of Technology has a long-standing reputation in DSL design and its verification. The group is well-known for its mCRL2 toolset, which is also used as a verification backend of many industrial development languages.
We are seeking a PhD student to join the research group to validate both the software restructurings developed during the project, as well as to validate software after restructuring. The main lines of research in this project are the post-translation validation of behavior of the software, possibly based on state transition graphs extracted from LLVM-IR, and the automated generation of test cases from such models using model-based test techniques.
We are looking for enthusiastic candidates who can contribute to the development of theoretical foundation, design and implementation of new validation techniques in the mCRL2 toolset, and the evaluation of these techniques in case studies.
The work in the project is supervised by Prof.dr.ir. Jan Friso Groote and dr.ir. Jeroen Keiren. The PhD student will collaborate with the PhD students from TU Delft, with co-applicants Eelco Visser and Casper Bach Poulsen at TU Delft, and Arjan Mooij from TNO/ESI.
We are looking for candidates that have:
We offer you:
Questions regarding the academic content of the position can be directed to:
More information on employment conditions can be found here:
All applications should include a PDF attachment with: