ในวิทยาการคอมพิวเตอร์การจำลองคือการคำนวณการทำงานของระบบการเปลี่ยนสถานะ ที่มีแบบจำลองที่เหมาะสม โดยทั่วไป กระบวนการนี้จะจำลองสถานะทั้งหมดของระบบ ณ จุดต่างๆ ในช่วงเวลาเชิงเส้นแบบไม่ต่อเนื่อง โดยคำนวณแต่ละสถานะตามลำดับจากสถานะก่อนหน้า แบบจำลองสำหรับโปรแกรมคอมพิวเตอร์หรือการออกแบบตรรกะ VLSI สามารถจำลองได้ง่ายมาก เนื่องจากมักมีความหมายเชิงปฏิบัติการที่สามารถนำมาใช้ในการจำลองได้โดยตรง

การจำลองเชิงสัญลักษณ์เป็นรูปแบบหนึ่งของการจำลองที่พิจารณาการทำงานที่เป็นไปได้หลายอย่างของระบบพร้อมกัน โดยทั่วไปจะทำได้โดยการขยายโดเมนที่ใช้ในการจำลอง สามารถใช้ ตัวแปร เชิงสัญลักษณ์ ในการแสดงสถานะการจำลองเพื่อจัดทำดัชนีการทำงานหลายอย่างของระบบ^{[ 1 ]}สำหรับค่าที่เป็นไปได้แต่ละค่าของตัวแปรเหล่านี้ จะมีสถานะระบบที่เป็นรูปธรรมที่ถูกจำลองทางอ้อม

เนื่องจากการจำลองเชิงสัญลักษณ์สามารถครอบคลุมการทำงานของระบบได้หลายครั้งในการจำลองเพียงครั้งเดียว จึงช่วยลดขนาดของปัญหาการตรวจสอบได้อย่างมาก เทคนิคต่างๆ เช่นการประเมินวิถีเชิงสัญลักษณ์ (STE) และการประเมินวิถีเชิงสัญลักษณ์แบบทั่วไป (GSTE) ล้วนมีพื้นฐานมาจากแนวคิดของการจำลองเชิงสัญลักษณ์นี้

• การประหารเชิงสัญลักษณ์
• การคำนวณเชิงสัญลักษณ์