Reasoning about loops using Vampire in KeY

DOI10.1007/978-3-662-48899-7_30zbMATH Open1471.68299OpenAlexW2230265119MaRDI QIDQ3460073FDOQ3460073

Authors: Wolfgang Ahrendt, Laura Kovács, Simon Robillard 

Publication date: 12 January 2016

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://research.chalmers.se/en/publication/230103

Recommendations

• Interpolation and symbol elimination in Vampire
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Ilinva: using abduction to generate loop invariants
• Synthesizing invariants by solving solvable loops
• Automating Verification of Loops by Parallelization

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (3)

• Automating Verification of Loops by Parallelization
• Lingva: generating and proving program properties using symbol elimination
• Ilinva: using abduction to generate loop invariants

Uses Software

• Dafny
• VAMPIRE
• Boogie
• InvGen
• KeY
• Lingva
• DynaMate

This page was built for publication: Reasoning about loops using Vampire in KeY

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460073)