Tarkvara analüüsi tehnika, kus programmi täitmise simuleeritakse, kasutades sümboleid nagu muutujate nimed, mitte tegelikud väärtused sisestatud andmete ja programmi väljundite väljendatakse loogiline või matemaatilisi avaldisi, kaasates need sümbolid.