Institute of Computer Languages
Compilers and Languages Group
on
| Date: | Wednesday, February 4th, 2009 |
|---|---|
| Time: | 16:30 |
| Location: | TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte) |
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 a recent article presented at the
2008 Austrian-Japan Workshop on Symbolic Computation in Software
Science. 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 de ne classes of verification conditions
which can be handled by other means and, if possible, hold also in
weaker theories than reals.
(This is joint work with Tudor Jebelean.)
Madalina Erascu is a 1st year PhD student in the Theorema research group (leader: Bruno Buchberger) at the Research Institute for Symbolic Computation (RISC), Johannes Kepler University of Linz, Austria. She is interested in program analysis using formal methods, computer algebra and automated theorem proving. She holds a M.Sc. from Johannes Kepler University (International School for Informatics), Linz. (http://www.risc.uni-linz.ac.at/home/merascu)
Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.