This paper introduces symbolic execution as a method for program testing and debugging. Symbolic execution involves replacing program inputs with symbolic expressions rather than numerical values, allowing the program to be executed in a way that explores all possible input combinations. The paper describes the EFFIGY system, which implements symbolic execution for program testing and debugging. EFFIGY supports symbolic execution of programs written in a PL/I-style language, includes debugging features, and allows for the verification of program correctness. It also discusses the relationship between symbolic execution and program proving, highlighting the challenges in reducing theoretical concepts to practical applications. Symbolic execution is a natural extension of normal execution, providing a way to explore all possible input paths through a program. It is particularly useful for testing programs with complex conditional logic, as it can generate test cases that cover a wide range of input scenarios. The paper explains how symbolic execution works, including the handling of conditional statements and the generation of path conditions. It also discusses the commutative property of symbolic execution, where the order of execution and instantiation of symbolic values does not affect the results. The paper provides examples of symbolic execution, including the SUM and POWER programs, and discusses the use of symbolic execution in program verification. It also addresses the challenges of symbolic execution, such as handling infinite execution trees and the need for case analysis in programs with complex control flow. The paper concludes that symbolic execution is a valuable tool for program testing and debugging, offering a practical approach between exhaustive testing and formal program proving. It also highlights the importance of symbolic execution in program analysis, including test case generation and optimization.This paper introduces symbolic execution as a method for program testing and debugging. Symbolic execution involves replacing program inputs with symbolic expressions rather than numerical values, allowing the program to be executed in a way that explores all possible input combinations. The paper describes the EFFIGY system, which implements symbolic execution for program testing and debugging. EFFIGY supports symbolic execution of programs written in a PL/I-style language, includes debugging features, and allows for the verification of program correctness. It also discusses the relationship between symbolic execution and program proving, highlighting the challenges in reducing theoretical concepts to practical applications. Symbolic execution is a natural extension of normal execution, providing a way to explore all possible input paths through a program. It is particularly useful for testing programs with complex conditional logic, as it can generate test cases that cover a wide range of input scenarios. The paper explains how symbolic execution works, including the handling of conditional statements and the generation of path conditions. It also discusses the commutative property of symbolic execution, where the order of execution and instantiation of symbolic values does not affect the results. The paper provides examples of symbolic execution, including the SUM and POWER programs, and discusses the use of symbolic execution in program verification. It also addresses the challenges of symbolic execution, such as handling infinite execution trees and the need for case analysis in programs with complex control flow. The paper concludes that symbolic execution is a valuable tool for program testing and debugging, offering a practical approach between exhaustive testing and formal program proving. It also highlights the importance of symbolic execution in program analysis, including test case generation and optimization.