Verification of Imperative Programs using Symbolic Execution and Forward Reasoning in the Theorema system Extended abstract

We present our work in progress concerning the verification of imperative programs in the Theorema system. Given an imperative program P and its specification (input condition formula IP and output condition formula OP), we are interested in finding the answer to the question: Is the program P correct with respect to its specification? To answer this question we use a method which is based on forward reasoning [4, 3], symbolic execution [2, 5] and functional semantics [7]. The program P is represented as a term at meta-level; it contains formulae and terms from the theory Υ in predicate logic and constructs corresponding to the imperative language statements. For writing imperative programs in Theorema system, we use some commands for the user interface role [6] (Program, Pre, Post, FwdVCG), which allow the definition of programs together with their specification, and imperative language constructs: � abrupt termination statements (return) � assignments- besides simple constant and variable assignment, function (including recursive call) call is also handled � conditionals: If with one and two branches Example Program["MyFactorial", Fact[ ↓ n], Module[{fact}]