Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal

Details:

   
TitleValigator: A verification tool with bound and invariant generation.
Author(s) Thomas A. Henzinger, Thibaud Hottelier, Levente Kovacs
TypeBook, Chapter in Book, Conference Proceeding
AbstractWe describe Valigator, a software tool for imperative program verification that efficiently combines symbolic computation and automated reasoning in a uniform framework. The system offers support for automatically generating and proving verification conditions and, most importantly, for automatically inferring loop invariants and bound assertions by means of symbolic summation, Gröbner basis computation, and quantifier elimination. We present general principles of the implementation and illustrate them on examples.
ISBN978-3-540-89438-4/pbk
URL http://link.springer.com/chapter/10.1007%2F978-3-540-89439-1_24
LanguageEnglish
Pages333--342
PublisherBerlin: Springer
Year2008
Edition0
Translation No
Refereed No
Webmaster