En programvara analys teknik där programkörningen simuleras med hjälp av symboler, t ex variabelnamn, snarare än faktiska värden för indata, och programmet utgångar är uttryckta som logiska eller matematiska uttryck med dessa symboler.