[Zurück]


Vorträge und Posterpräsentationen (ohne Tagungsband-Eintrag):

L. Kovacs:
"Experiments with Invariant Generation Using a Saturation Theorem Prover";
Vortrag: "Deduction at Scale" Seminar, Ringberg Castle, Germany (eingeladen); 07.03.2011 - 11.03.2011.



Kurzfassung deutsch:
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.

Kurzfassung englisch:
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.

Schlagworte:
program verification, loop invariants, theorem proving

Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.