Symbol Elimination for Automated Generation of Program Properties

Laura Kovacs

Abstract


Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this talk we describe applications of our symbol elimination methods in automated proram analysis. Symbol elimination uses first-order theorem proving techniques in conjunction with symbolic computation methods, and derives nontrivial program properties, such as loop invariants and loop bounds, in a fully automatic way. Moreover, symbol elimination can be used as an alternative to interpolation for software verification.

Full Text:

PDF


DOI: http://dx.doi.org/10.14279/tuj.eceasst.70.974

DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.70.974.952

Hosted By Universit├Ątsbibliothek TU Berlin.