Abstraction via Program Transformation - Lauko, Henrich (2023)
V oblasti autonomní verifikace programů jsou abstrakční techniky nezbytné, protože hrají kritickou roli při snižování složitosti verifikačního procesu na zvládnutelné velikosti. Tyto techniky jsou však obvykle pevně integrovány do nástrojů, což vede k nežádoucí složitosti a opomenutí opakovaně použitelného návrhu. Pokud chce někdo použít konkrétní abstrakci v několika nástrojích, běžným přístupem je implementovat abstrakci zvlášť pro každý nástroj. To však vede k zbytečné duplikaci úsilí a nekonzistentním výsledkům, protože různé implementace se mohou lišit. Tato dizertační práce si klade za cíl řešit tuto výzvu vytvořením řešení pro snížení duplikace a složitosti abstrakce. Hlavním cílem je vytvořit nástrojově nezávislou abstrakci programu a využít ji k návrhu technik analýzy programu, které mohou být aplikovány libovolným nástrojem, čímž se snižuje složitost a umožňuje opakované použití abstrakce. To, co mají nástroje společné, je reprezentace programu, se kterou pracují. Jedna tako