Formally Certifying the Security of Digital Signature Schemes. - Santiago Zanella-Béguelin; Gilles Barthe; Benjamin Grégoire; Federico Olmedo (SP, 2009)

Verifiable Security of Boneh-Franklin Identity-Based Encryption. - Gilles Barthe; Federico Olmedo; Santiago Zanella-Béguelin (ProvSec, 2011)

Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs. - Gilles Barthe; Federico Olmedo (ICALP (2), 2013)

Verified indifferentiable hashing into elliptic curves. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; Federico Olmedo; Santiago Zanella-Béguelin (J. Comput. Secur., 2013)

Probabilistic Relational Reasoning for Differential Privacy. - Gilles Barthe; Boris Köpf; Federico Olmedo; Santiago Zanella-Béguelin (ACM Trans. Program. Lang. Syst., 2013)

Approximate Relational Reasoning for Probabilistic Programs. - Federico Olmedo (2014)

Understanding Probabilistic Programs. - Joost-Pieter Katoen; Friedrich Gretz; Nils Jansen 001; Benjamin Lucien Kaminski; Federico Olmedo (Correct System Design, 2015)

Conditioning in Probabilistic Programming. - Nils Jansen 001; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Federico Olmedo; Friedrich Gretz; Annabelle McIver (MFPS, 2015)

Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Federico Olmedo (ESOP, 2016)

Reasoning about Recursive Probabilistic Programs. - Federico Olmedo; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (LICS, 2016)

Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Federico Olmedo (J. ACM, 2018)

Runtime Analysis of Quantum Programs: A Formal Approach. - Federico Olmedo; Alejandro Díaz-Caro (CoRR, 2019)

A mechanized formalization of GraphQL. - Tomás Díaz; Federico Olmedo; Éric Tanter (CPP, 2020)

Contextual Linear Types for Differential Privacy. - Matías Toro; David Darais; Chike Abuah; Joe Near; Federico Olmedo; Éric Tanter (CoRR, 2020)

Slicing of Probabilistic Programs Based on Specifications (Extended Abstract). - Marcelo Navarro; Federico Olmedo (ECOOP, 2022)

Slicing of probabilistic programs based on specifications. - Marcelo Navarro; Federico Olmedo (Sci. Comput. Program., 2022)

A Gradual Probabilistic Lambda Calculus. - Wenjia Ye; Matías Toro; Federico Olmedo (Proc. ACM Program. Lang., 2023)

Contextual Linear Types for Differential Privacy. - Matías Toro; David Darais; Chike Abuah; Joseph P. Near; Damián Árquez; Federico Olmedo; Éric Tanter (ACM Trans. Program. Lang. Syst., 2023)

Static Slicing for Probabilistic Programs: An Overview. - Federico Olmedo (Principles of Verification (1), 2024)

Differential privacy and SPARQL. - Carlos Buil-Aranda; Jorge Lobo 001; Federico Olmedo (Semantic Web, 2024)

Gradual Differentially Private Programming. - Matías Toro; Federico Olmedo; Éric Tanter (Commun. ACM, 2024)