An Arithmetic Theory for the Poly-Time Random Functions. - Melissa Antonelli; Ugo Dal Lago; Davide Davoli 001; Isabel Oitavem; Paolo Pistone (CoRR, 2023)

On Kernel's Safety in the Spectre Era (And KASLR is Formally Dead). - Davide Davoli 001; Martin Avanzini; Tamara Rezk (CCS, 2024)

On Separation Logic, Computational Independence, and Pseudorandomness. - Ugo Dal Lago; Davide Davoli 001; Bruce M. Kapron (CSF, 2024)

Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories. - Melissa Antonelli; Ugo Dal Lago; Davide Davoli 001; Isabel Oitavem; Paolo Pistone (CSL, 2024)

On Separation Logic, Computational Independence, and Pseudorandomness (Extended Version). - Ugo Dal Lago; Davide Davoli 001; Bruce M. Kapron (CoRR, 2024)

On Kernel's Safety in the Spectre Era (Extended Version). - Davide Davoli 001; Martin Avanzini; Tamara Rezk (CoRR, 2024)

Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation (Extended Version). - Davide Davoli 001; Martin Avanzini; Tamara Rezk (CoRR, 2024)

A Quantitative Probabilistic Relational Hoare Logic. - Martin Avanzini; Gilles Barthe; Davide Davoli 001; Benjamin Grégoire (Proc. ACM Program. Lang., 2025)