Talks and Poster Presentations (without Proceedings-Entry):
L. Kovacs:
"Experiments with Invariant Generation Using a Saturation Theorem Prover";
Talk: "Deduction at Scale" Seminar,
Ringberg Castle, Germany (invited);
2011-03-07
- 2011-03-11.
English abstract:
We evaluate invariant generation technique using symbol elimination in the combination of first order logic and various theories.
The technique is using the first-order theorem prover Vampire
for both generating invariants and minimising the set of
generated invariants.
We discuss implementation details of invariant generation in
Vampire and present experimental results obtained on academic and industrial
benchmarks. The results demonstrate the power of the symbol
elimination method in generating quantified invariants.
German abstract:
We evaluate invariant generation technique using symbol elimination in the combination of first order logic and various theories.
The technique is using the first-order theorem prover Vampire
for both generating invariants and minimising the set of
generated invariants.
We discuss implementation details of invariant generation in
Vampire and present experimental results obtained on academic and industrial
benchmarks. The results demonstrate the power of the symbol
elimination method in generating quantified invariants.
Keywords:
program verification, loop invariants, theorem proving
Created from the Publication Database of the Vienna University of Technology.