Institute of Computer Languages
Compilers and Languages Group

Talks 2009 - Madalina Erascu

The Compilers and Languages Group invites you to a talk given by

Madalina Erascu, M.Sc.

RISC-Linz, Johannes Kepler University, Linz, Austria

on

Forward Symbolic Execution for Program Verification in Theorema System

Date: Wednesday, February 4th, 2009
Time: 16:30
Location: TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte)

Abstract:

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.)

About Madalina Erascu, M.Sc.:

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.

Complang
   About Us
   Research
   Lehre
   Service
      Robotics
      Library
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Sitemap
Contact
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)