Zobrazeno 1 - 10 of 10 pro vyhledávání: '"Aymeric Fromherz"'
1
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Autor: Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Nikhil Swamy
Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, 2020, 4 (ICFP), pp.1-30. ⟨10.1145/3409003⟩
Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (ICFP), pp.1-30. ⟨10.1145/3409003⟩
CONICET Digital (CONICET)
Consejo Nacional de Investigaciones Científicas y Técnicas
instacron:CONICET
Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logi
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4b5ec170330922c1708301920abfc1c0
http://arxiv.org/abs/2111.15149
Zobrazit plný text záznamu
2
Steel: proof-oriented programming in a dependently typed concurrent separation logic
Autor: Nikhil Swamy, Tahina Ramananandro, Guido Martínez, Aymeric Fromherz, Aseem Rastogi, Denis Merigoux, Sydney Gibson
Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (ICFP), pp.1-30. ⟨10.1145/3473590⟩
Proceedings of the ACM on Programming Languages, 2021, 5 (ICFP), pp.1-30. ⟨10.1145/3473590⟩
Steel is a language for developing and proving concurrent programs embedded in F ⋆ , a dependently typed programming language and proof assistant. Based on SteelCore, a concurrent separation logic (CSL) formalized in F ⋆ , our work focuses on exp
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bf75c2af3c958224646b3ddfe90140d4
https://hal.inria.fr/hal-03466397
Zobrazit plný text záznamu
3
Turning Catala into a Proof Platform for the Law
Autor: Alain Delaët, Denis Merigoux, Aymeric Fromherz
Publikováno v: POPL 2022-Programming Languages and the Law
POPL 2022-Programming Languages and the Law, Jan 2022, Philadelphia, United States
HAL
International audience
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::32a459678c890fac169337ed1440d1eb
https://hal.inria.fr/hal-03447072/file/paper.pdf
Zobrazit plný text záznamu
5
A verified, efficient embedding of a verifiable assembly language
Autor: Aseem Rastogi, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Nikhil Swamy, Nick Giannarakis
Publikováno v: Proceedings of the ACM on Programming Languages. 3:1-30
High-performance cryptographic libraries often mix code written in a high-level language with code written in assembly. To support formally verifying the correctness and security of such hybrid programs, this paper presents an embedding of a subset o
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::9c88f32b3bd2ba3fff9e7d1ba0fdb9fe
https://doi.org/10.1145/3290376
Zobrazit plný text záznamu
6
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Autor: Nikhil Swamy, Antoine Delignat-Lavaud, Jonathan Protzenko, Joonwon Choi, Bryan Parno, Christoph M. Wintersteiger, Chris Hawblitzel, Aseem Rastogi, Natalia Kulatova, Aymeric Fromherz, Marina Polubelova, Santiago Zanella-Béguelin, Tahina Ramananandro, Karthikeyan Bhargavan, Benjamin Beurdouche, Cédric Fournet
Publikováno v: SP 2020-IEEE Symposium on Security and Privacy
SP 2020-IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.983-1002, ⟨10.1109/SP40000.2020.00114⟩
IEEE Symposium on Security and Privacy
2020 IEEE Symposium on Security and Privacy (SP)
International audience; We present EverCrypt: a comprehensive collection of verified, high-performance cryptographic functionalities available via a carefully designed API. The API provably supports agility (choosing between multiple algorithms for t
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b754b12d09129b9fb446c4bb80a284b0
https://inria.hal.science/hal-03154278
Zobrazit plný text záznamu
7
Symbolic Arrays in Symbolic PathFinder
Autor: Corina S. Păsăreanu, Aymeric Fromherz, Kasper Søe Luckow
Publikováno v: ACM SIGSOFT Software Engineering Notes. 41:1-5
Symbolic Execution is a program analysis technique used to increase software reliability. Modern software often manipulate complex data structures, many of which being similar to arrays. We present a novel approach and implementation in Symbolic Path
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::b627792fd454792ad031348ce2cdf30c
https://doi.org/10.1145/3011286.3011296
Zobrazit plný text záznamu
8
Symbolic Pathfinder for SV-COMP
Autor: Yannic Noller, Xuan-Bach D. Le, Willem Visser, Aymeric Fromherz, Corina S. Păsăreanu
Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030175016
TACAS (3)
This paper describes the benchmark entry for Symbolic Pathfinder, a symbolic execution tool for Java bytecode. We give a brief description of the tool and we describe the particular run configuration that was used in the SV-COMP competition. Furtherm
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::392893748015d3d5ea21c19799ea323a
https://doi.org/10.1007/978-3-030-17502-3_21
Zobrazit plný text záznamu
9
Static Value Analysis of Python Programs by Abstract Interpretation
Autor: Abdelraouf Ouadjaout, Aymeric Fromherz, Antoine Miné
Publikováno v: Lecture Notes in Computer Science
Lecture Notes in Computer Science-NASA Formal Methods
NASA Formal Methods
NASA Formal Methods 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings
NFM 2018-10th International Symposium NASA Formal Methods
NFM 2018-10th International Symposium NASA Formal Methods, Apr 2018, Newport News, VA, United States. pp.185-202, ⟨10.1007/978-3-319-77935-5_14⟩
Lecture Notes in Computer Science ISBN: 9783319779348
NFM
International audience; We propose a static analysis by abstract interpretation for a significant subset of Python to infer variable values, run-time errors, and uncaught exceptions. Python is a high-level language with dynamic typing, a class-based
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::64c0266cdeb0160f1f062862774708fe
Zobrazit plný text záznamu
10
HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms)
Autor: Santiago Zanella-Béguelin, Natalia Kulatova, Benjamin Beurdouche, Marina Polubelova, Jonathan Protzenko, Aymeric Fromherz, Karthikeyan Bhargavan
Publikováno v: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security
CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security
CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, Nov 2020, Virtual Event, United States
CCS
We present a new methodology for building formally verified cryptographic libraries that are optimized for multiple architectures. In particular, we show how to write and verify generic crypto code in the F* programming language that exploits single-
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::466bf443eba0c55eb5a40cdc48be11f3
Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání

Omezení vyhledávání
Plný text Recenzováno Digitální knihovna AV ČR
Zdroje