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

Akademický článek

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.

Autor: Georges, Aïna Linn¹ algeorges@mpi-sws.org, Guéneau, Armaël² armael.gueneau@inria.fr, Van Strydonck, Thomas³ thomas.vanstrydonck@cs.kuleuven.be, Timany, Amin⁴ timany@cs.au.dk, Trieu, Alix⁵ alix.trieu@ssi.gouv.fr, Devriese, Dominique³ dominique.devriese@kuleuven.be, Birkedal, Lars⁴ birkedal@cs.au.dk

Publikováno v: Journal of the ACM. Feb2024, Vol. 71 Issue 1, p1-59. 59p.

Zobrazit plný text záznamu

Report

The ins and outs of iteration in Mezzo

Autor: Guéneau, Armaël, Pottier, François, Protzenko, Jonathan

This is a talk proposal for HOPE 2013. Using iteration over a collection as a case study, we wish to illustrate the strengths and weaknesses of the prototype programming language Mezzo.

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

Zobrazit plný text záznamu

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code

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

A capability machine is a type of CPU allowing fine-grained privilege separation using capabilities, machine words that represent certain kinds of authority. We present a mathematical model and accompanying proof methods that can be used for formal v

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______165::1cff7364922398b7cb44bb4b949e8da2
https://hal.science/hal-03826854/document

Zobrazit plný text záznamu

Vérification mécanisée de la correction et complexité asymptotique de programmes

Autor: Guéneau, Armaël

Publikováno v: Programming Languages [cs.PL]. Université de Paris, 2019. English
Logic in Computer Science [cs.LO]. Université de Paris, 2019. English. ⟨NNT : 2019UNIP7110⟩
Programming Languages [cs.PL]. Université de Paris, 2019. English. ⟨NNT : ⟩

This dissertation is concerned with the question of formally verifying that the imple- mentation of an algorithm is not only functionally correct (it always returns the right result), but also has the right asymptotic complexity (it reliably computes

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::0701e7b2b4ac715f4bfa754dc2ff9a04
https://hal.inria.fr/tel-02437532/document

Zobrazit plný text záznamu

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

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

Publikováno v: 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=od_______212::1d1458a707191efd01b3d0e48480626b
https://hal.inria.fr/hal-02167236

Zobrazit plný text záznamu

Procrastination: A proof engineering technique

Autor: Guéneau, Armaël

Publikováno v: Coq Workshop 2018
Coq Workshop 2018, Jul 2018, Oxford, United Kingdom

The Coq Workshop 2018 is a part of FLoC 2018; International audience; We present a small Coq library for collecting side conditions and deferring their proof.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::367e6db92085d61f6a45d8a8ced8b84e
https://inria.hal.science/hal-01962659/document

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání