User-interactive undo is a recovery facility that enables users to correct mistakes easily by canceling or re-executing operations that have already been executed. This paper presents an interesting common structural property that has been discovered in programs that implementing user-interactive undo features. The property shows that there is a one-to-one correspondence between program statements that raise erroneous effects and those statements that can undo these effects. Statistical validation has been conducted which gives evidences to show that this property holds for 99 per cent of all the cases. An approach for automated verification of user-interactive undo features in database applications through the use of this empirical property is further proposed. Based on the verification results, test cases are automatically generated to confirm the correctness of these features. A case study has been conducted to evaluate the performance of the proposed verification and testing approach in terms of fault detection capability.