Search: onr:"swepub:oai:research.chalmers.se:31118c7d-81c8-4c0f-bd6e-a2022d141fcd" >
Reasoning About Loo...
Reasoning About Loops Using Vampire in KeY
-
- Ahrendt, Wolfgang, 1967 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Kovacs, Laura, 1980 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Robillard, Simon, 1989 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- ISBN 9783662488980
- 2015-11-22
- 2015
- English.
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783662488980 ; 9450, s. 434-443
- Related links:
-
http://publications.... (primary) (free)
-
show more...
-
http://publications....
-
https://research.cha...
-
https://doi.org/10.1...
-
show less...
Abstract
Subject headings
Close
- We describe symbol elimination and consequence finding in the first-order theorem prover Vampire for automatic generation of quantified invariants, possibly with quantifier alternations, of loops with arrays. Unlike the previous implementation of symbol elimination in Vampire, our work is not limited to a specific programming language but provides a generic framework by relying on a simple guarded command representation of the input loop. We also improve the loop analysis part in Vampire by generating loop properties more easily handled by the saturation engine of Vampire. Our experiments show that, with our changes, the number of generated invariants is decreased, in some cases, by a factor of 20. We also provide a framework to use our approach to invariant generation in conjunction with pre- and post-conditions of program loops. We use the program specification to find relevant invariants as well as to verify the partial correctness of the loop. As a case study, we demonstrate how symbol elimination in Vampire can be used as an interface for realistic imperative languages, by integrating our tool inthe KeY verification system, thus allowing reasoning about loops in Java programs in a fully automated way, without any user guidance.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Publication and Content Type
- kon (subject category)
- ref (subject category)
Find in a library
To the university's database