Ilinva: using abduction to generate loop invariants

DOI10.1007/978-3-030-29007-8_5MaRDI QIDQ2180218zbMATH OpenOpenAlexFDO

Authors Mnacho Echenim, Nicolas Peltier, Yanis Sellami

Publication date 13 May 2020

Full work available at URL https://arxiv.org/abs/1906.11033

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)

Abstract: We describe a system to prove properties of programs. The key feature of this approach is a method to automatically synthesize inductive invariants of the loops contained in the program. The method is generic, i.e., it applies to a large set of programming languages and application domains; and lazy, in the sense that it only generates invariants that allow one to derive the required properties. It relies on an existing system called GPiD for abductive reasoning modulo theories, and on the platform for program verification Why3. Experiments show evidence of the practical relevance of our approach.

Recommendations

• Synthesizing invariants by solving solvable loops
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Reasoning about loops using Vampire in KeY
• Computer Aided Verification
• From program verification to program synthesis

Cited in

(9)

• Scalable algorithms for abduction via enumerative syntax-guided synthesis
• Lingva: generating and proving program properties using symbol elimination
• Reasoning about loops using Vampire in KeY
• Inferring Loop Invariants Using Postconditions
• Automatic generation of non-linear loop invariants
• Synthesis of circular compositional program proofs via abduction
• Automatically inferring loop invariants via algorithmic learning
• An interactive SMT tactic in Coq using abductive reasoning
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs

This page was built for publication: Ilinva: using abduction to generate loop invariants

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