Formula rewriting systems and their application to automated program verification

We describe a notion of formula rewriting systems (FRSs) and investigate a relation between FRSs and techniques of term rewriting systems (TRSs) and narrowing. We demonstrate the use of FRSs for finding errors in array and file operations.