Computerprogramma's zijn over het algemeen moeilijk foutloos te maken. Zelfs de meest ervaren programmeurs maken soms fouten. Bij programma-analyse wordt gekeken naar verschillende aspecten van het gedrag van het programma, wat helpt om de betrouwbaarheid van programma's te verbeteren. Dit promotieonderzoek gaat over terminatieanalyse. Het is niet gericht op een specifieke programmeertaal, maar gaat over termherschrijfsystemen (term rewriting systems; TRS's). Logisch beperkte simpel getypeerde TRS's (logically constrained simply-typed TRSs; LCSTRS's) worden geïntroduceerd, een hoger-ordeformalisme dat primitieve datatypes ondersteunt door middel van logische restricties, en hun terminatie wordt geanalyseerd. De niet-modulariteit van terminatie vormt een grote uitdaging. We kunnen namelijk niet in het algemeen concluderen dat een samengesteld systeem als geheel termineert op basis van de terminatie van alle afzonderlijke delen, en het is niet altijd mogelijk om het gehele systeem in één keer te analyseren. Om deze uitdaging aan te pakken, wordt in dit promotieonderzoek de dependency pair (DP)-methode uitgebreid naar LCSTRS's. In dit promotieonderzoek wordt ook een andere dimensie van modulariteit in terminatieanalyse onderzocht, namelijk de analyse van een module in een programma zonder voorafgaande kennis over hoe precies de functies die het definieert in andere delen van het programma kunnen worden gebruikt. Om de kloof tussen TRS's en programma's uit de praktijk verder te overbruggen, behandelt dit promotieonderzoek bovendien herschrijven volgens call-by-value op LCSTRS's.
Liye Guo begon in 2020 met zijn promotieonderzoek aan de Radboud Universiteit onder begeleiding van Cynthia Kop en Herman Geuvers. Voordat hij naar Nederland verhuisde, behaalde hij zijn bachelordiploma aan de University of Science and Technology of China en zijn masterdiploma aan de University of Utah.