Validating the Z specification of Telephone Book System with symbolic execution

Symbolic execution has been used as a technique to validate telephone book specification system. A set of test case has been prepared to integrate with telephone book specification system for validation process. Supports from ztc and Z/EVES have assisted this study to get a very precise, and concise results thus reduce human error. Findings through this study are very crucial in order to raise more confidence using symbolic execution as a technique to validate formal specification.