SYMBOLIC EXECUTION AND EQUIVALENCE TESTING