关注
Pierre-Yves Strub
Pierre-Yves Strub
Research Scientist, PQShield
在 strub.nu 的电子邮件经过验证 - 首页
标题
引用次数
年份
12th International Conference on Interactive Theorem Proving (ITP 2021)
MO Myreen, N Polikarpova, A Popescu, T Bauereiss, P Lammich, ...
Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, 2021
2021
A calculus of congruent constructions
F Blanqui, JP Jouannaud, PY Strub
Unpublished draft, 2005
82005
A drag-and-drop proof tactic
P Donato, PY Strub, B Werner
Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022
152022
A formal disproof of hirsch conjecture
X Allamigeon, Q Canu, PY Strub
Proceedings of the 12th ACM SIGPLAN International Conference on Certified …, 2023
42023
A formal library for elliptic curves in the Coq proof assistant
EI Bartzia, PY Strub
International Conference on Interactive Theorem Proving, 77-92, 2014
222014
A Formalization of the Proof of Correctness of a Number-Theoretic Transform in the Context of the Hakyber Cryptographic Primitive
A Séré, PY Strub
Journées 2022 du GT” Méthodes Formelles pour la Sécurité”, GdR Sécurité …, 2022
2022
A machine-checked proof of security for AWS key management service
JB Almeida, M Barbosa, G Barthe, M Campagna, E Cohen, B Gregoire, ...
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications …, 2019
262019
A messy state of the union
B Beurdouche, A Delignat-Lavaud, C Fournet, M Kohlweiss, A Pironti, ...
1
A messy state of the union: taming the composite state machines of TLS
K Bhargavan, B Beurdouche, A Delignat-Lavaud, C Fournet, M Kohlweiss, ...
Communications of the ACM 60 (2), 99-107, 2017
2017
A messy state of the union: Taming the composite state machines of TLS
B Beurdouche, K Bhargavan, A Delignat-Lavaud, C Fournet, M Kohlweiss, ...
Communications of the ACM 60 (2), 99-107, 2017
4042017
A program logic for probabilistic programs
G Barthe, T Espitau, M Gaboardi, B Grégoire, J Hsu, PY Strub
Available at justinh. su/files/papers/ellora. pdf, 2016
82016
A program logic for union bounds
G Barthe, M Gaboardi, B Grégoire, J Hsu, PY Strub
arXiv preprint arXiv:1602.05681, 2016
342016
A relational logic for higher-order programs
A Aguirre, G Barthe, M Gaboardi, D Garg, PY Strub
Proceedings of the ACM on Programming Languages 1 (ICFP), 1-29, 2017
682017
A Relational Logic for Higher-Order Programs (Additional material)
A AGUIRRE, G BARTHE, M GABOARDI, D GARG, PY STRUB
2017
A Tight Security Proof for , Formally Verified
M Barbosa, F Dupressoir, A Hülsing, M Meijers, PY Strub
Cryptology ePrint Archive, 2024
2024
Actema: une interface graphique et gestuelle pour preuves formelles (démonstration)
P Donato, PY Strub, B Werner
33èmes Journées Francophones des Langages Applicatifs, 267-268, 2022
2022
Advanced probabilistic couplings for differential privacy
G Barthe, N Fong, M Gaboardi, B Grégoire, J Hsu, PY Strub
Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications …, 2016
632016
An assertion-based program logic for probabilistic programs
G Barthe, T Espitau, M Gaboardi, B Grégoire, J Hsu, PY Strub
Programming Languages and Systems: 27th European Symposium on Programming …, 2018
302018
An implementation of TLS 1.2 with verified cryptographic security
C Fournet, K Bhargavan, M Kohlweiss, A Pironti, PY Strub
Proceedings of the Second international conference on Principles of Security …, 2013
12013
Building decision procedures in the calculus of inductive constructions
F Blanqui, JP Jouannaud, PY Strub
Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual …, 2007
242007
系统目前无法执行此操作,请稍后再试。
文章 1–20