Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

10 résultats
Page :
triés par
Image document

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

 Aïna Linn Georges , Armaël Guéneau , Thomas Van Strydonck , Amin Timany , Alix Trieu , et al.
Journal of the ACM (JACM), 2023, ⟨10.1145/3623510⟩
Article dans une revue hal-03826854v3

Theorems for free from separation logic specifications

 Lars Birkedal , Thomas Dinsdale-Young , Armaël Guéneau , Guilhem Jaber , Kasper Svendsen , et al.
Proceedings of the ACM on Programming Languages, 2021, 5 (ICFP), pp.1-29. ⟨10.1145/3473586⟩
Article dans une revue hal-03510684v1
Image document

The Logical Essence of Well-Bracketed Control Flow

 Amin Timany , Armaël Guéneau , Lars Birkedal
POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages, SIGPLAN, Jan 2024, Londres, United Kingdom
Communication dans un congrès hal-04271457v1
Image document

Thunks and Debits in Separation Logic with Time Credits

 François Pottier , Armaël Guéneau , Jacques-Henri Jourdan , Glen Mével
POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages, SIGPLAN, Jan 2024, Londres, United Kingdom
Communication dans un congrès hal-04238691v2
Image document

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

 Armaël Guéneau , Arthur Charguéraud , François Pottier
ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. ⟨10.1007/978-3-319-89884-1_19⟩
Communication dans un congrès hal-01926485v1
Image document

Proving full-system security properties under multiple attacker models on capability machines

 Thomas Van Strydonck , Aïna Linn Georges , Armaël Guéneau , Alix Trieu , Amin Timany , et al.
CSF 2022 - 35th IEEE Computer Security Foundations Symposium, Aug 2022, Haifa, Israel
Communication dans un congrès hal-03826851v1
Image document

Mechanized Verification of the Correctness and Asymptotic Complexity of Programs

 Armaël Guéneau
Programming Languages [cs.PL]. Université de Paris, 2019. English. ⟨NNT : ⟩
Thèse tel-02437532v1

The ins and outs of iteration in Mezzo

 Armaël Guéneau , François Pottier , Jonathan Protzenko
2013
Pré-publication, Document de travail hal-00912381v1
Image document

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C

 Armaël Guéneau , Johannes Hostert , Simon Spies , Michael Sammler , Lars Birkedal , et al.
OOPSLA 2023 - Object-Oriented Programming, Systems, Languages & Applications 2023, SIGPLAN, Oct 2023, Cascais, Portugal. ⟨10.1145/3622823⟩
Communication dans un congrès hal-04203298v2
Image document

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

 Armaël Guéneau , Jacques-Henri Jourdan , Arthur Charguéraud , François Pottier
Interactive Theorem Proving, Sep 2019, Portland, United States
Communication dans un congrès hal-02167236v1
Page :