Valigator: A verification tool with bound and invariant generation Conference Paper


Author(s): Henzinger, Thomas A; Hottelier, Thibaud; Kovács, Laura
Title: Valigator: A verification tool with bound and invariant generation
Title Series: LNCS
Affiliation
Abstract: We 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.
Conference Title: LPAR: Logic for Programming, Artificial Intelligence, and Reasoning
Volume: 5330
Conference Dates: November 22-27, 2008
Conference Location: Doha, Qatar
ISBN: 978-3-642-45220-8
Publisher: Springer  
Location: Berlin, Heidelberg
Date Published: 2008-11-13
Start Page: 333
End Page: 342
Sponsor: This research was supported by the Swiss NSF.
URL:
DOI: 10.1007/978-3-540-89439-1_24
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work