Symbolic Execution is a concept which has gained traction recently due to the advances in constraint solving and increasing computational power, which can be used for Formal Verification.

Roughly speaking, it executes the program using symbolic values (variables) instead of actual inputs, and as the execution proceeds it gathers constraints on the symbols. Given a precondition and postcondition, we can use rules of inference to verify whether the constraints gather imply the postcondition, assuming it starts from the precondition.

There are many tools available for symbolic execution, which can handle fairly large codebases and are used in the industry, although many of the use cases arise from a cybersecurity perspective.

Symbolic Execution is a concept which has gained traction due to the advances in constraint solving, increasing computational power and recently DARPA Cyber Grand Challenge, which can be used for Formal Verification.

Roughly speaking, it executes the program using symbolic values (variables) instead of actual inputs, and as the execution proceeds it gathers constraints on the symbols. Given a precondition and postcondition, we can use rules of inference to verify whether the constraints gather imply the postcondition, assuming it starts from the precondition.

There are many tools available for symbolic execution, which can handle fairly large codebases and are used in the industry, although many of the use cases arise from a cybersecurity perspective.