2 papers
cs.LO2019
Ilinva: Using Abduction to Generate Loop Invariants
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
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 pr…
cs.LO2018
A Generic Framework for Implicate Generation Modulo Theories
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
The clausal logical consequences of a formula are called its implicates. The generation of these implicates has several applications, such as the identification of missing hypothes…