Reasoning about loops using Vampire in KeY

DOI10.1007/978-3-662-48899-7_30MaRDI QIDQ3460073zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(3)

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

Describes a project that uses

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)