Raisonnement abductif modulo des théories et application à la vérification de programmes

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______2592::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