Use of symbolic program execution in program testing

Abstract

In recent years, we have increasing activity in the field of program verification. The goal of these efforts is to create computer systems to determine whether the given computer program is correct, in terms of meeting the given specifications. Program testing is in principle a complicated process that must be carried out as systematically as possible, to provide adequate proof of the reliability and quality. Specification is a key thing in program testing. This work describes methods used for constructive testing of smaller programs. One of the ways to prove whether a given program is properly written is the symbolic execution of program.