author = {L. Kovacs and N. Popov and T. Jebelean},
title = {{Verification Environment in Theorema}},
language = {english},
abstract = {We present a verification environment for imperative programs (using Hoare logic) and for functional programs (using fixpoint theory) in the frame of the Theorema system (www.theorema.org). In particular, we discuss some methods for finding the invariants of loops and specifications of auxiliary tail recursive functions. These methods use techniques from (polynomial) algebra and combinatorics, namely Groebner bases, variable elimination and symbolic summation (the Gosper algorithm, the technique of generating functions). The methods are demonstrated on several examples which have been treated automatically by our mplementation. },
journal = {Annals of Mathematics, Computing and Teleinformatics (AMCT)},
volume = {1},
number = {2},
pages = {27--34},
isbn_issn = {ISSN 1109-9305},
year = {2005},
refereed = {yes},
length = {8},
url = {http://journals.teilar.gr/amct/}