Program Behavior Discovery and Verification: A Graph Grammar Approach