We present a static analysis method for imperative program verification based on forward symbolic execution; given the Hoare triple (Input Specification, Program Body, Output Specification), we want to check whether the program fulfils its specification. The problem of generating the verification conditions is approached using an axiomatic calculus characterizing inference rules for each statement encountered in the program: assignments (including recursive calls), conditionals and abrupt statements (Return). While loops can be simulated using conditionals and recursion. Detailed theoretical aspects of this method are stated in [1]. The method is implemented in a prototype framework on top of the computer algebra system Mathematica and uses the existing Theorema imperative language. Our goal is to automatically prove/disprove the verification conditions generated using logical, algebraic and combinatorial techniques. At this aim, we combined logical (natural deduction) and simple algebraic inferences for preprocessing the verification conditions. For further reasoning about the resulting formulae, we will use polynomial algebra algorithms which might (e.g. Cylindrical Algebraic CAD Decomposition works on the theory of real closed fields) or might not (e.g. Groebner basis algorithms works on a commutative ring with 1) need to set an underlying theory. Although CAD method is powerful enough for handling our formulae, it has a high complexity and therefore we avoid to use it until the latest. We will define classes of verification conditions which can be handled by other means and, if possible, hold also in weaker theories than reals.
| [1] | M. Erascu and T. Jebelean. Practical Program Verification by Forward Symbolic Execution: Correctness and Examples. In B. Buchberger, T. Ida, T. Kutsia, editors, Proceedings of Austrian-Japan Workshop on Symbolic Computation in Software Science, pages 47-56, 2008. |
Tudor Jebelean is an Associate Professor in the Theorema group (leader: Bruno Buchberger and Tudor Jebelean) at the Research Institute for Symbolic Computation (RISC), Johannes Kepler University of Linz, Austria. His main research interests are automated reasoning and program verification using logic and algebraic methods. He holds a PhD in Computer Science and Habilitation title from Johannes Kepler University of Linz.
Contact Madalina and Tudor at:
Madalina Erascu, M.Sc.
Research Institute for Symbolic Computation (RISC)
Johannes Kepler University of Linz
A-4040 Linz, Austria
merasc at risc.uni-linz.ac.at
http://www.risc.uni-linz.ac.at/home/merascu/
Prof. Dr. Tudor Jebelean
Research Institute for Symbolic Computation (RISC)
Johannes Kepler University of Linz
A-4040 Linz, Austria
Tudor.Jebelean at risc.uni-linz.ac.at
http://www.risc.uni-linz.ac.at/home/tjebelea/