En software analyse teknik hvor programafviklingen simuleres ved hjælp af symboler, som variabelnavne, snarere end faktiske værdier for input-data, og programmet udgange er udtrykt som logisk eller matematiske udtryk, der involverer disse symboler.