Výsledky vyhledávání - "Armaël Guéneau"

Theorems for free from separation logic specifications

Autor: Guilhem Jaber, Nikos Tzevelekos, Thomas Dinsdale-Young, Kasper Svendsen, Armaël Guéneau, Lars Birkedal

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (ICFP), pp.1-29. ⟨10.1145/3473586⟩
Birkedal, L, Dinsdale-Young, T, Guéneau, A, Jaber, G, Svendsen, K & Tzevelekos, N 2021, ' Theorems for free from separation logic specifications ', Proceedings of the ACM on Programming Languages, vol. 5, no. ICFP, 81 . https://doi.org/10.1145/3473586
Proceedings of the ACM on Programming Languages, 2021, 5 (ICFP), pp.1-29. ⟨10.1145/3473586⟩

International audience; Separation logic specifications with abstract predicates intuitively enforce a discipline that constrains when and how calls may be made between a client and a library. Thus a separation logic specification of a library intuit

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e35f5012f890d1efb00d735a96ce54c2
https://hal.archives-ouvertes.fr/hal-03510684

Zobrazit plný text záznamu

Cap’ ou pas cap’ ?

Autor: Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal

Publikováno v: Georges, A L, Guéneau, A, Van Strydonck, T, Timany, A, Trieu, A, Devriese, D & Birkedal, L 2021, Cap’ ou pas cap’ ?: Preuve de programmes pour une machine à capacités en présence de code inconnu . i Journées Francophones des Langages Applicatifs 2021 . Institut de Recherche en Informatique Fondamentale, Journées Francophones des Langages Applicatifs 2021, 07/04/2021 . < https://researchportal.vub.be/en/publications/cap-ou-pas-cap-preuve-de-programmes-pour-une-machine-%C3%A0-capacit%C3%A9s->
Aarhus University

Une machine à capacités est un type de microprocesseur permettant une séparation des permissions précise grâce à l’utilisation de capacités, mots machine porteurs d’une certaine autorité. Dans cet article, nous présentons une méthode pe

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::71c592db4ae94c8e161299186a7b67db
https://biblio.vub.ac.be/vubir/(c96b23ca-0972-4fec-ae4c-c9b7dd8db4ad).html

Zobrazit plný text záznamu

Efficient and Provable Local Capability Revocation using Uninitialized Capabilities

Autor: Sander Huyghebaert, Alix Trieu, Dominique Devriese, Lars Birkedal, Amin Timany, Armaël Guéneau, Thomas Van Strydonck, Aïna Linn Georges

Publikováno v: Georges, A L, Guéneau, A, Van Strydonck, T, Timany, A, Trieu, A, Huyghebaert, S, Devriese, D & Birkedal, L 2021, ' Efficient and provable local capability revocation using uninitialized capabilities ', Proceedings of the ACM on Programming Languages, vol. 5, no. POPL, 6 . https://doi.org/10.1145/3434287

Capability machines are a special form of CPUs that offer fine-grained privilege separation using a form of authority-carrying values known as capabilities. The CHERI capability machine offers local capabilities, which could be used as a cheap but re

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3c781525403e7d6f014d001abcfdd8ac
https://lirias.kuleuven.be/handle/123456789/679781

Zobrazit plný text záznamu

Iris Mechanization of a Local Capability Machine with Uninitialized Capabilities

Autor: Georges, Aina Linn, Armaël Guéneau, Strydonck, Thomas Van, Timany, Amin, Trieu, Alix

The Iris mechanization contains all the definitions and proofs presented in the paper "Efficient and Provable Local Capability Revocation using Uninitialized Capabilities" The zipped folder contains all of the source code, and the VM image contains a

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

Zobrazit plný text záznamu

A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification

Autor: Armaël Guéneau, Arthur Charguéraud, François Pottier

Publikováno v: ESOP 2018-27th European Symposium on Programming
ESOP 2018-27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. ⟨10.1007/978-3-319-89884-1_19⟩
Programming Languages and Systems ISBN: 9783319898834
ESOP

Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018; International audience; We present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of hig

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::abd852d52d9b9f3c07b68a55e74fe72c
https://inria.hal.science/hal-01926485

Zobrazit plný text záznamu

Verified Characteristic Formulae for CakeML

Autor: Ramana Kumar, Michael Norrish, Armaël Guéneau, Magnus O. Myreen

Publikováno v: Programming Languages and Systems ISBN: 9783662544334
ESOP

Characteristic Formulae (CF) offer a productive, principled approach to generating verification conditions for higher-order imperative programs, but so far the soundness of CF has only been considered with respect to an informal specification of a pr

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::af2545cd78613482f1282661217cdc50
https://doi.org/10.1007/978-3-662-54434-1_22

Zobrazit plný text záznamu

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm: (extended version)

Autor: Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier

Publikováno v: HAL
Leibniz International Proceedings in Informatics
Interactive Theorem Proving
Interactive Theorem Proving, Sep 2019, Portland, United States

International audience; We study a state-of-the-art incremental cycle detection algorithm due to Bender, Fineman, Gilbert, and Tarjan. We propose a simple change that allows the algorithm to be regarded as genuinely online. Then, we exploit Separatio

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::51ded3b6bbe8081d3008750ad78a98de
https://hal.inria.fr/hal-02167236

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání