Abductive reasoning modulo theories and an application to program verification

Autor: Sellami, Yanis

Publikováno v: Data Structures and Algorithms [cs.DS]. Université Grenoble Alpes [2020-..], 2020. English. ⟨NNT : 2020GRALM018⟩

This thesis introduces a generic method to compute the prime implicates of a logical formula, i.e., the most general clausal consequences of a given logical formula, in any given decidable theory. The principle used is to recursively add to an initia

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______212::f339f76577a1094bd55348e0e61ab695
https://tel.archives-ouvertes.fr/tel-02990726/document

On Symbolic Heaps Modulo Permission Theories

Autor: Demri, S, Lozes, E, Lugiez, Denis

Publikováno v: 37th IARCS Foundation on Software Technology and Theoretical Computer Science
37th IARCS Foundation on Software Technology and Theoretical Computer Science, Dec 2017, Kanpur, India. ⟨10.4230/LIPIcs.FSTTCS.2017.25⟩

International audience; We address the entailment problem for separation logic with symbolic heaps admitting list predicates and permissions for memory cells that are essential to express ownership of a heap region. In the permission-free case, the e

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f753c5929d748b352fdce62ae44620f0

Ilinva: Using Abduction to Generate Loop Invariants

Autor: Echenim, Mnacho, Peltier, Nicolas, Sellami, Yanis

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 progr

Externí odkaz: http://arxiv.org/abs/1906.11033

First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice.

Autor: Burel, Guillaume, Bury, Guillaume, Cauderlier, Raphaël, Delahaye, David, Halmagrand, Pierre, Hermant, Olivier

Publikováno v: Journal of Automated Reasoning; Aug2020, Vol. 64 Issue 6, p1001-1050, 50p

Programming Logics : Essays in Memory of Harald Ganzinger

Autor: Andrei Voronkov, Christoph Weidenbach

This Festschrift volume, published in memory of Harald Ganzinger, contains 17 papers from colleagues all over the world and covers all the fields to which Harald Ganzinger dedicated his work during his academic career. The volume begins with a comple