Davide Davoli

12 papers A* 1A 1B 1Journal 8
YearRankTypeTitle / Venue / Authors
2025 J jnl
A Quantitative Probabilistic Relational Hoare Logic.
Proc. ACM Program. Lang.
Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire
2025 J jnl
Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation.
ACM Trans. Priv. Secur.
Davide Davoli, Martin Avanzini, Tamara Rezk
2025 — —
Provable security for kernels and cryptography in the presence of speculative execution. (Sécurité prouvable pour les noyaux et cryptographie en présence d'exécution spéculative).
Davide Davoli
2024 J jnl
A quantitative probabilistic relational Hoare logic.
CoRR
Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire
2024 J jnl
Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation (Extended Version).
CoRR
Davide Davoli, Martin Avanzini, Tamara Rezk
2024 B conf
Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories.
CSL
Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, Paolo Pistone
2024 A* conf
On Kernel's Safety in the Spectre Era (And KASLR is Formally Dead).
CCS
Davide Davoli, Martin Avanzini, Tamara Rezk
2024 J jnl
On Kernel's Safety in the Spectre Era (Extended Version).
CoRR
Davide Davoli, Martin Avanzini, Tamara Rezk
2024 J jnl
On Separation Logic, Computational Independence, and Pseudorandomness (Extended Version).
CoRR
Ugo Dal Lago, Davide Davoli, Bruce M. Kapron
2024 A conf
On Separation Logic, Computational Independence, and Pseudorandomness.
CSF
Ugo Dal Lago, Davide Davoli, Bruce M. Kapron
2023 J jnl
An Arithmetic Theory for the Poly-Time Random Functions.
CoRR
Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, Paolo Pistone
2023 J jnl
Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories.
CoRR
Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, Paolo Pistone