Correctness of program transformations

Description of the research topic:

Program source code can be represented in various models and may be transformed with various algorithms to improve code quality while preserving the program’s observable behaviour. Modern IDE’s do offer so-called refactoring steps to increase programmers’ productivity, but lack any formal guarantees on correctness (i.e. the refactoring preserves the program behaviour). In fact, providing formal correctness proofs for complex refactoring steps is an open research question. The main goal of the research is to design methods and tools for formally defining programming languages, program models, static analysis and program rewriting, and use these to formally reason about refactoring correctness.

Thesis supervisor: Dániel Horpácsi

Required language skills: English
Further requirements: Familiarity with the following subjects: functional programming, compilers, formal semantics, static analyis, rewrite calculi, mathematical logic, formal verification.

How to Apply?

If you are interested apply here: [PhD] Doctoral School of Informatics – Eötvös Loránd University (elte.hu)

For more information visite the following website: Doctoral School of Informatics (elte.hu)

Only local Hubs members can access this page. Join the community today: https://archive.phdhub.eu/register