Skip to content  

Working at TU/e

PhD student in Validating Software Restructurings

PhD student in Validating Software Restructurings

The Eindhoven University of Technology Department of Mathematics & Computer Science has an open position for a PhD student in the Formal System Analysis group in the area of Validating Software Restructurings.
Department of Mathematics & Computer Science
Graduate Program(s)
Computer Science
Date off
Reference number

Job description

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.

Project Organization

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 Jan Friso Groote and 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.

Job requirements

We are looking for candidates that have:

  • A master’s degree (or equivalent) in computer science (or closely related fields);
  • A strong and demonstrable affinity for formal methods, including experience with topics such as model checking and behavioral equivalences and/or model-based testing;
  • A strong interest in programming languages and software development;
  • A strong commitment to turning theory into software and demonstrable software engineering skills (with object-oriented and functional programming languages) to realize that;
  • Independent, self-motivated, reliable, and eager to learn;
  • Ability to work in a project team and take leadership and responsibility for different research tasks;
  • An excellent command of English and good academic writing and presentation skills.

Conditions of employment

We offer you:

  • An exciting job in a dynamic work environment
  • The opportunity to closely collaborate with industrial and academic partners
  • A fixed-term, full-time contract for four years at Eindhoven University of Technology
  • The salary is in accordance with the Collective Labour Agreement of the Dutch Universities, increasing from € 2.325 per month initially, to € 2.972 in the fourth year.
  • An attractive package of fringe benefits, including end-of-year bonus (8,3% in December), an extra holiday allowance (8% in May), moving expenses and excellent sports facilities.

Information and application

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:

  • an application letter, including a statement of research interests that demonstrates an understanding of the project topic;
  • a detailed CV (including list of publications if available);
  • a list of courses taken and grades obtained;
  • a copy or link to your Master’s thesis;
  • contact details of 2-3 references