טכניקת ניתוח תוכנה שבה ביצוע התוכנית מדומה באמצעות סימנים, כגון שמות משתנים, ולא ערכים בפועל עבור נתוני קלט, והתפוקות התוכנית באים לידי ביטוי כביטויים לוגית או מתמטית מעורבים סמלים אלו.