Skip to Main content Skip to Navigation
Conference papers

Ilinva: Using Abduction to Generate Loop Invariants

Mnacho Echenim 1 Nicolas Peltier 1 Yanis Sellami 1
1 CAPP - Calculs algorithmes programmes et preuves
LIG - Laboratoire d'Informatique de Grenoble [2007-2015]
Abstract : We describe a system to prove properties of programs. The key feature of this approach is a method to automatically synthesize in-ductive 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 [14], and on the platform for program verification Why3 [16]. Experiments show evidence of the practical relevance of our approach.
Document type :
Conference papers
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download
Contributor : Nicolas Peltier <>
Submitted on : Tuesday, November 5, 2019 - 10:07:43 AM
Last modification on : Thursday, July 9, 2020 - 9:44:45 AM
Document(s) archivé(s) le : Thursday, February 6, 2020 - 6:30:09 PM


Files produced by the author(s)




Mnacho Echenim, Nicolas Peltier, Yanis Sellami. Ilinva: Using Abduction to Generate Loop Invariants. Frontiers of Combining Systems - 12th International Symposium, 2019, London, United Kingdom. pp.77-93, ⟨10.1007/978-3-030-29007-8_5⟩. ⟨hal-02323446⟩



Record views


Files downloads