A programok forráskódját sokféle modellben ábrázolhatjuk, továbbá több különböző algoritmussal átalakíthatjuk úgy, hogy a forráskód minőségét javítsuk, de közben az eredeti program viselkedését megőrizzük. Ezeket az úgynevezett refaktorálás műveleteket sok kódszerkesztő eszköz támogatja, de helyes működésre (tehát a programjelentés megőrzésére) vonatkozóan ritkán adnak formális garanciákat. Valójában összetett refaktorálások helyességének igazolása egy mai napig nyitott kérdés. A kutatás fő célja a gyakorlatban alkalmazott refaktorálási műveletek megbízhatóságának növelése programozási nyelvek, programmodellek, statikus elemzések és programátírások jelentésének formális megfogalmazásával, majd formális érveléssel a programátírások helyességére vonatkozóan.
előírt nyelvtudás: angol ajánlott nyelvtudás (magyar oldal): angol további elvárások: Jártasság a következő témákban: funkcionális programozás, fordítóprogramok, formális szemantika, statikus elemzés, átíró kalkulusok, logikai nyelvek, formális helyességbizonyítás.