Federico Olmedo

Federico Olmedo is an Assistant Professor at the Computer Science Department of the University of Chile, where he teaches courses like Program Analysis and Verification (CC4101) and Discrete Mathematics for Computer Science (CC3101). His research focuses on the semantics and verification of probabilistic programs, with applications in language-based security, differential privacy, and formal verification of cryptographic systems. Previously, he was a postdoctoral researcher at RWTH Aachen University and earned his PhD from the Technical University of Madrid in 2014.

Research Interests:

• Program Verification
• Probabilistic Programming
• Language-Based Security
• Theorem Provers
• Quantum Computing
• Cryptographic Proofs

Publications span formal methods for probabilistic programs, including weakest precondition calculi, runtime analysis of quantum programs, and machine-checked proofs for cryptographic protocols. Notable works include the Best Theory Paper Award at ECOOP 2016 and foundational research on conditioning in probabilistic programming. He co-developed the CertiCrypt and CertiPriv frameworks for verifying cryptographic proofs and differential privacy in Coq.

Scientific Awards:

• ECOOP 2016 Best Theory Paper Award