Federico Olmedo
Assistant Professor
Computer Science Department, University of Chile
Young Researcher
Millennium Institute Foundational Research on Data
Computer Science Department, University of Chile
Young Researcher
Millennium Institute Foundational Research on Data
FCFM - Universidad de Chile
Oficina 311 Norte (DCC)
Av. Beauchef 851
Santiago, Chile
folmedo@dcc.uchile.cl
(+56) 22 9784975
Research Interests
I am interested in the semantics and verification of programs in general, and in particular, in the verification of probabilistic programs. More specifically, my research interests are:
- Program semantics and verification
- Probabilistic programming
- Differential privacy
- Language-based security
Publications
For more detailed information about my publications, please consult my DBLP or Google Scholar entry.
Program slicing aims to simplify programs by identifying and removing non-essential parts while preserving program behavior. It is widely used for program understanding, debugging, and software maintenance. This article provides an overview of slicing techniques for probabilistic programs, which blend traditional programming constructs with random sampling and conditioning. These programs have experienced a notable resurgence in recent years due to new applications in fields such as artificial intelligence and differential privacy.
Concretely, we review the three major slicing techniques currently available for probabilistic programs: the foundational technique by Hur et al., the subsequent development by Amtoft and Banerjee based on probabilistic control flow graphs, and the more recent approach by Navarro and Olmedo based on program specifications. We provide a clear, accessible, and self-contained presentation of these techniques, and compare them across multiple dimensions to provide a deeper insight into the current state-of-the-art in probabilistic program slicing.
Concretely, we review the three major slicing techniques currently available for probabilistic programs: the foundational technique by Hur et al., the subsequent development by Amtoft and Banerjee based on probabilistic control flow graphs, and the more recent approach by Navarro and Olmedo based on program specifications. We provide a clear, accessible, and self-contained presentation of these techniques, and compare them across multiple dimensions to provide a deeper insight into the current state-of-the-art in probabilistic program slicing.
This article presents a novel approach to combining gradual typing with differential privacy (DP) to facilitate the development and verification of privacy-preserving programs. We introduce a gradual sensitivity type discipline that allows programmers to begin with unknown or partially annotated sensitivities and refine them incrementally, thereby unifying static and dynamic checking. Our approach naturally accommodates programs—including recursive ones—whose sensitivity depends on runtime values, and we establish key properties such as gradual metric preservation and soundness. Finally, we provide a prototype implementation demonstrating the practicality of our method and discuss how it paves the way for integrating DP into mainstream programming environments.
Differential privacy is a framework that provides formal tools to develop algorithms to access databases and answer statistical queries with quantifiable accuracy and privacy guarantees. The notions of differential privacy are defined independently of the data model and the query language at steak. Most differential privacy results have been obtained on aggregation queries such as counting or finding maximum or average values, and on grouping queries over aggregations such as the creation of histograms. So far, the data model used by the framework research has typically been the relational model and the query language SQL. However, effective realizations of differential privacy for SQL queries that required joins had been limited. This has imposed severe restrictions on applying differential privacy in RDF knowledge graphs and SPARQL queries. By the simple nature of RDF data, most useful queries accessing RDF graphs will require intensive use of joins. Recently, new differential privacy techniques have been developed that can be applied to many types of joins in SQL with reasonable results. This opened the question of whether these new results carry over to RDF and SPARQL. In this paper we provide a positive answer to this question by presenting an algorithm that can answer counting queries over a large class of SPARQL queries that guarantees differential privacy, if the RDF graph is accompanied with semantic information about its structure. We have implemented our algorithm and conducted several experiments, showing the feasibility of our approach for large graph databases. Our aim has been to present an approach that can be used as a stepping stone towards extensions and other realizations of differential privacy for SPARQL and RDF.
Program slicing aims to simplify programs by identifying and removing non-essential parts while preserving program behavior. It is widely used for program understanding, debugging, and software maintenance. This paper provides an overview of slicing techniques for probabilistic programs, which blend traditional programming constructs with random sampling and conditioning. These programs have experienced a notable resurgence in recent years due to new applications in fields such as differential privacy and artificial intelligence.
We particularly focus on backward static slicing techniques, the most traditional form of program slicing. We review the foundational technique by Hur et al. and the subsequent developments by Amtoft and Banerjee, based on probabilistic control flow graphs. Through motivating examples and sketches of key definitions and results, we provide a clear, accessible, and self-contained presentation of slicing techniques for probabilistic programs.
We particularly focus on backward static slicing techniques, the most traditional form of program slicing. We review the foundational technique by Hur et al. and the subsequent developments by Amtoft and Banerjee, based on probabilistic control flow graphs. Through motivating examples and sketches of key definitions and results, we provide a clear, accessible, and self-contained presentation of slicing techniques for probabilistic programs.
Probabilistic programming languages have recently gained a lot of attention, in particular due to their applications in domains such as machine learning and differential privacy. To establish invariants of interest, many such languages include some form of static checking in the form of type systems. However, adopting such a type discipline can be cumbersome or overly conservative. Gradual typing addresses this problem by supporting a smooth transition between static and dynamic checking, and has been successfully applied for languages with different constructs and type abstractions. Nevertheless, its benefits have never been explored in the context of probabilistic languages.
In this work, we present and formalize GPLC, a gradual source probabilistic lambda calculus. GPLC includes a binary probabilistic choice operator and allows programmers to gradually introduce/remove static type—and probability—annotations. The static semantics of GPLC heavily relies on the notion of probabilistic couplings, as required for defining several relations, such as consistency, precision, and consistent transitivity. The dynamic semantics of GPLC is given via elaboration to the target language TPLC, which features a distribution-based semantics interpreting programs as probability distributions over final values. Regarding the language metatheory, we establish that TPLC—and therefore also GPLC—is type safe and satisfies two of the so-called refined criteria for gradual languages, namely, that it is a conservative extension of a fully static variant and that it satisfies the gradual guarantee, behaving smoothly with respect to type precision.
In this work, we present and formalize GPLC, a gradual source probabilistic lambda calculus. GPLC includes a binary probabilistic choice operator and allows programmers to gradually introduce/remove static type—and probability—annotations. The static semantics of GPLC heavily relies on the notion of probabilistic couplings, as required for defining several relations, such as consistency, precision, and consistent transitivity. The dynamic semantics of GPLC is given via elaboration to the target language TPLC, which features a distribution-based semantics interpreting programs as probability distributions over final values. Regarding the language metatheory, we establish that TPLC—and therefore also GPLC—is type safe and satisfies two of the so-called refined criteria for gradual languages, namely, that it is a conservative extension of a fully static variant and that it satisfies the gradual guarantee, behaving smoothly with respect to type precision.
Language support for differentially private programming is both crucial and delicate. While elaborate program logics can be very expressive, type-system-based approaches using linear types tend to be more lightweight and amenable to automatic checking and inference, and in particular in the presence of higher-order programming. Since the seminal design of Fuzz, which is restricted to ϵ-differential privacy in its original design, significant progress has been made to support more advanced variants of differential privacy, like (ϵ, δ)-differential privacy. However, supporting these advanced privacy variants while also supporting higher-order programming in full has proven to be challenging. We present Jazz, a language and type system that uses linear types and latent contextual effects to support both advanced variants of differential privacy and higher-order programming. Latent contextual effects allow delaying the payment of effects for connectives such as products, sums, and functions, yielding advantages in terms of precision of the analysis and annotation burden upon elimination, as well as modularity. We formalize the core of Jazz, prove it sound for privacy via a logical relation for metric preservation, and illustrate its expressive power through a number of case studies drawn from the recent differential privacy literature.
We present the first slicing approach for probabilistic programs based on specifications. Concretely, we show that when probabilistic programs are accompanied by their functional specifications in the form of pre- and post-condition, one can exploit this semantic information to produce specification-preserving slices strictly more precise than slices yielded by conventional techniques based on data/control dependency.
Our slicing technique works by propagating post-conditions backward using the greatest pre-expectation transformer—the probabilistic counterpart of Dijkstra’s weakest pre-condition transformer. This provides an axiomatic semantics via a verification condition generator (VCGen) that yields quantitative proof obligations.
VCGens are developed (and proved sound) for both partial and total correctness of probabilistic programs, making our slicing technique termination-sensitive. The approach requires loop invariants and probabilistic variants for reasoning about (probabilistic) termination. Modularity ensures valid slices are computable locally for subprograms.
Besides developing the theoretical foundations, we present an algorithm for computing least slices using shortest-path techniques and demonstrate applicability via illustrative examples and a probabilistic modeling case study.
Our slicing technique works by propagating post-conditions backward using the greatest pre-expectation transformer—the probabilistic counterpart of Dijkstra’s weakest pre-condition transformer. This provides an axiomatic semantics via a verification condition generator (VCGen) that yields quantitative proof obligations.
VCGens are developed (and proved sound) for both partial and total correctness of probabilistic programs, making our slicing technique termination-sensitive. The approach requires loop invariants and probabilistic variants for reasoning about (probabilistic) termination. Modularity ensures valid slices are computable locally for subprograms.
Besides developing the theoretical foundations, we present an algorithm for computing least slices using shortest-path techniques and demonstrate applicability via illustrative examples and a probabilistic modeling case study.
GraphQL is a novel language for specifying and querying web APIs, allowing clients to flexibly and efficiently retrieve data of interest. The GraphQL language specification is unfortunately only available in prose, making it hard to develop robust formal results for this language. Recently, Hartig and Pérez proposed a formal semantics for GraphQL in order to study the complexity of GraphQL queries. The semantics is however not mechanized and leaves certain key aspects unverified. We present GraphCoQL, the first mechanized formalization of GraphQL, developed in the Coq proof assistant. GraphCoQL covers the schema definition DSL, query definitions, validation of both schema and queries, as well as the semantics of queries over a graph data model. We illustrate the application of GraphCoQL by formalizing the key query transformation and interpretation techniques of Hartig and Pérez, and proving them correct, after addressing some imprecisions and minor issues. We hope that GraphCoQL can serve as a solid formal baseline for both language design and verification efforts for GraphQL.
In this abstract we study the resource consumption of quantum programs. Specifically, we focus on the expected runtime of programs and, inspired by recent methods for probabilistic programs, we develop a calculus à la weakest precondition to formally and systematically derive the (exact) expected runtime of quantum programs. Notably, the calculus admits a notion of loop runtime invariant that can be readily used to derive upper bounds of their runtime. Finally, we show the applicability of our calculus analyzing the runtime of (a simplified version of) the BB84 quantum key distribution protocol.
This article presents a wp–style calculus for obtaining bounds on the expected runtime of randomized algorithms. Its application includes determining the (possibly infinite) expected termination time of a randomized algorithm and proving positive almost–sure termination—does a program terminate with probability one in finite expected time? We provide several proof rules for bounding the runtime of loops, and prove the soundness of the approach with respect to a simple operational model. We show that our approach is a conservative extension of Nielson’s approach for reasoning about the runtime of deterministic programs. We analyze the expected runtime of some example programs including the coupon collector’s problem, a one–dimensional random walk and a randomized binary search.
This paper investigates the semantic intricacies of conditioning, a main feature in probabilistic programming. Our study is based on an extension of the imperative probabilistic guarded command language pGCL with conditioning. We provide a weakest pre–condition (wp) semantics and an operational semantics. To deal with possibly diverging program behaviour we consider liberal pre–conditions. We show that diverging program behaviour plays a key role when defining conditioning. We establish that weakest pre–conditions coincide with conditional expected rewards in Markov chains—the operational semantics—and that the wp–semantics conservatively extends the existing semantics of pGCL (without conditioning). An extension of these results with non–determinism turns out to be problematic: although an operational semantics using Markov decision processes is rather straightforward, we show that providing an inductive wp–semantics in this setting is impossible. Finally, we present two program transformations which eliminate conditioning from any program. The first transformation hoists conditioning while updating the probabilistic choices in the program, while the second transformation replaces conditioning—in the same vein as rejection sampling—by a program with loops. In addition, a program transformation is presented that replaces an independent identically distributed loop by conditioning.
This paper presents a wp-style calculus for obtaining bounds on the expected run-time of probabilistic programs. Its application includes determining the possibly infinite expected termination time of a probabilistic program and proving positive almost-sure termination--does a program terminate with probability one in finite expected time? We provide several proof rules for bounding the run-time of loops, and prove the soundness of the approach with respect to a simple operational model. We show that our approach is a conservative extension of Nielson's approach for reasoning about the run-time of deterministic programs. We analyze the expected run-time of some example programs including a one-dimensional random walk and the coupon collector problem.
This paper presents a wp-style calculus for obtaining expectations on the outcomes of (mutually) recursive probabilistic programs. We provide several proof rules to derive one- and two-sided bounds for such expectations, and show the soundness of our wp-calculus with respect to a probabilistic pushdown automaton semantics. We also give a wp-style calculus for obtaining bounds on the expected runtime of recursive programs that can be used to determine the (possibly infinite) time until termination of such programs.
In this paper, we investigate the semantic intricacies of conditioning in probabilistic programming, a major feature, e.g., in machine learning. We provide a quantitative weakest pre–condition semantics. In contrast to all other approaches, non–termination is taken into account by our semantics. We also present an operational semantics in terms of Markov models and show that expected rewards coincide with quantitative pre–conditions. A program transformation that entirely eliminates conditioning from programs is given; the correctness is shown using our semantics. Finally, we show that an inductive semantics for conditioning in non–deterministic probabilistic programs cannot exist.
We present two views of probabilistic programs and their relationship. An operational interpretation as well as a weakest pre-condition semantics are provided for an elementary probabilistic guarded command language. Our study treats important features such as sampling, conditioning, loop divergence, and non-determinism.
Many cryptographic systems based on elliptic curves are proven secure in the Random Oracle Model, assuming there exist probabilistic functions that map elements in some domain (e.g. bitstrings) onto uniformly and independently distributed points in a curve. When implementing such systems, and in order for the proof to carry over to the implementation, those mappings must be instantiated with concrete constructions whose behavior does not deviate significantly from random oracles. In contrast to other approaches to public-key cryptography, where candidates to instantiate random oracles have been known for some time, the first generic construction for hashing into ordinary elliptic curves indifferentiable from a random oracle was put forward only recently by Brier et al. We present a machine-checked proof of this construction. The proof is based on an extension of the CertiCrypt framework with logics and mechanized tools for reasoning about approximate forms of observational equivalence, and integrates mathematical libraries of group theory and elliptic curves.
Differential privacy is a notion of confidentiality that allows useful computations on sensible data while protecting the privacy of individuals. Proving differential privacy is a difficult and error-prone task that calls for principled approaches and tool support. Approaches based on linear types and static analysis have recently emerged; however, an increasing number of programs achieve privacy using techniques that fall out of their scope. Examples include programs that aim for weaker, approximate differential privacy guarantees and programs that achieve differential privacy without using any standard mechanisms. Providing support for reasoning about the privacy of such programs has been an open problem.
We report on CertiPriv, a machine-checked framework for reasoning about differential privacy built on top of the Coq proof assistant. The central component of CertiPriv is a quantitative extension of probabilistic relational Hoare logic that enables one to derive differential privacy guarantees for programs from first principles. We demonstrate the applicability of CertiPriv on a number of examples whose formal analysis is out of the reach of previous techniques. In particular, we provide the first machine-checked proofs of correctness of the Laplacian, Gaussian, and exponential mechanisms and of the privacy of randomized and streaming algorithms from the literature.
We report on CertiPriv, a machine-checked framework for reasoning about differential privacy built on top of the Coq proof assistant. The central component of CertiPriv is a quantitative extension of probabilistic relational Hoare logic that enables one to derive differential privacy guarantees for programs from first principles. We demonstrate the applicability of CertiPriv on a number of examples whose formal analysis is out of the reach of previous techniques. In particular, we provide the first machine-checked proofs of correctness of the Laplacian, Gaussian, and exponential mechanisms and of the privacy of randomized and streaming algorithms from the literature.
f-divergences form a class of measures of distance between probability distributions; they are widely used in areas such as information theory and signal processing. In this paper, we unveil a new connection between f-divergences and differential privacy, a confidentiality policy that provides strong privacy guarantees for private data-mining; specifically, we observe that the notion of α-distance used to characterize approximate differential privacy is an instance of the family off-divergences. Building on this observation, we generalize to arbitrary f-divergences the sequential composition theorem of differential privacy. Then, we propose a relational program logic to prove upper bounds for the f-divergence between two probabilistic programs. Our results allow us to revisit the foundations of differential privacy under a new light, and to pave the way for applications that use different instances of f-divergences.
Many cryptographic systems based on elliptic curves are proven secure in the Random Oracle Model, assuming there exist probabilistic functions that map elements in some domain (e.g. bitstrings) onto uniformly and independently distributed points in a curve. When implementing such systems, and in order for the proof to carry over to the implementation, those mappings must be instantiated with concrete constructions whose behavior does not deviate significantly from random oracles. In contrast to other approaches to public-key cryptography, where candidates to instantiate random oracles have been known for some time, the first generic construction for hashing into ordinary elliptic curves indifferentiable from a random oracle was put forward only recently by Brier et al. We present a machine-checked proof of this construction. The proof is based on an extension of the CertiCrypt framework with logics and mechanized tools for reasoning about approximate forms of observational equivalence, and integrates mathematical libraries of group theory and elliptic curves.
Differential privacy is a notion of confidentiality that protects the privacy of individuals while allowing useful computations on their private data. Deriving differential privacy guarantees for real programs is a difficult and error-prone task that calls for principled approaches and tool support. Approaches based on linear types and static analysis have recently emerged; however, an increasing number of programs achieve privacy using techniques that cannot be analyzed by these approaches. Examples include programs that aim for weaker, approximate differential privacy guarantees, programs that use the Exponential mechanism, and randomized programs that achieve differential privacy without using any standard mechanism. Providing support for reasoning about the privacy of such programs has been an open problem.
We report on CertiPriv, a machine-checked framework for reasoning about differential privacy built on top of the Coq proof assistant. The central component of CertiPriv is a quantitative extension of a probabilistic relational Hoare logic that enables one to derive differential privacy guarantees for programs from first principles. We demonstrate the expressiveness of CertiPriv using a number of examples whose formal analysis is out of the reach of previous techniques. In particular, we provide the first machine-checked proofs of correctness of the Laplacian and Exponential mechanisms and of the privacy of randomized and streaming algorithms from the recent literature.
We report on CertiPriv, a machine-checked framework for reasoning about differential privacy built on top of the Coq proof assistant. The central component of CertiPriv is a quantitative extension of a probabilistic relational Hoare logic that enables one to derive differential privacy guarantees for programs from first principles. We demonstrate the expressiveness of CertiPriv using a number of examples whose formal analysis is out of the reach of previous techniques. In particular, we provide the first machine-checked proofs of correctness of the Laplacian and Exponential mechanisms and of the privacy of randomized and streaming algorithms from the recent literature.
Identity-based encryption (IBE) allows one party to send ciphered messages to another using an arbitrary identity string as an encryptionkey.Since IBE does not require prior generation and distribution of keys, it greatly simplifies key management in public-key cryptography. Although the concept of IBE was introduced by Shamir in 1981, constructing a practical IBE scheme remained an open problem for years. The first satisfactory solution was proposed by Boneh and Franklin in 2001 and constitutes one of the most prominent applications of pairingbased cryptography. We present a game-based machine-checked reduction of the security of the Boneh-Franklin IBE scheme to the Bilinear Diffie-Hellman assumption, and analyze its tightness by providing an exact security bound. Our proof simplifies and clarifies the original proof by Boneh and Franklin and can be automatically verified by running a trusted checker.
We present two machine-checked proofs of the existential unforgeability under adaptive chosen-message attacks of the FullDomain Hash signature scheme. These proofs formalize the original argument of Bellare and Rogaway, and an optimal reduction by Coronthat provides a tighter bound on the probability of a forgery. Both proofs are developed using CertiCrypt, a general framework toformalize exact security proofs of cryptographic systems in the computational model. Since CertiCrypt is implemented on top of theCoq proof assistant, the proofs are highly trustworthy and can be verified independently and fully automatically.
PhD Thesis
The verified security methodology is an emerging approach to
build high assurance proofs about security properties of
computer systems. Computer systems are modeled as probabilistic
programs and one relies on rigorous program semantics techniques to
prove that they comply with a given security goal. In particular, it
advocates the use of interactive theorem provers or automated provers
to build fully formal machine-checked versions of these security
proofs.
The verified security methodology has proved successful in modeling and reasoning about several standard security notions in the area of cryptography. However, it has fallen short of covering an important class of approximate, quantitative security notions. The distinguishing characteristic of this class of security notions is that they are stated as a "similarity" condition between the output distributions of two probabilistic programs, and this similarity is quantified using some notion of distance between probability distributions.
This class comprises prominent security notions from multiple areas such as private data analysis, information flow analysis and cryptography. These include, for instance, indifferentiability, which enables securely replacing an idealized component of system with a concrete implementation, and differential privacy, a notion of privacy-preserving data mining that has received a great deal of attention in the last few years. The lack of rigorous techniques for verifying these properties is thus an important problem that needs to be addressed.
In this dissertation we introduce several quantitative program logics to reason about this class of security notions. Our main theoretical contribution is, in particular, a quantitative variant of a full-fledged relational Hoare logic for probabilistic programs. The soundness of these logics is fully formalized in the Coq proof-assistant and tool support is also available through an extension of CertiCrypt, a framework to verify cryptographic proofs in Coq.
We validate the applicability of our approach by building fully machine-checked proofs for several systems that were out of the reach of the verified security methodology. These comprise, among others, a construction to build "safe" hash functions into elliptic curves and differentially private algorithms for several combinatorial optimization problems from the recent literature.
The verified security methodology has proved successful in modeling and reasoning about several standard security notions in the area of cryptography. However, it has fallen short of covering an important class of approximate, quantitative security notions. The distinguishing characteristic of this class of security notions is that they are stated as a "similarity" condition between the output distributions of two probabilistic programs, and this similarity is quantified using some notion of distance between probability distributions.
This class comprises prominent security notions from multiple areas such as private data analysis, information flow analysis and cryptography. These include, for instance, indifferentiability, which enables securely replacing an idealized component of system with a concrete implementation, and differential privacy, a notion of privacy-preserving data mining that has received a great deal of attention in the last few years. The lack of rigorous techniques for verifying these properties is thus an important problem that needs to be addressed.
In this dissertation we introduce several quantitative program logics to reason about this class of security notions. Our main theoretical contribution is, in particular, a quantitative variant of a full-fledged relational Hoare logic for probabilistic programs. The soundness of these logics is fully formalized in the Coq proof-assistant and tool support is also available through an extension of CertiCrypt, a framework to verify cryptographic proofs in Coq.
We validate the applicability of our approach by building fully machine-checked proofs for several systems that were out of the reach of the verified security methodology. These comprise, among others, a construction to build "safe" hash functions into elliptic curves and differentially private algorithms for several combinatorial optimization problems from the recent literature.
External Services
Conference Program Committee
- ECOOP 2025: 39th European Conference on Object-Oriented Programming
- LSFA 2021: 16th International Symposium on Logical and Semantic Frameworks with Applications
- FM 2019: 23rd International Symposium on Formal Methods
- SETTA 2019: 5th International Symposium on Software Engineering Theories, Tools, and Applications
Conference External Reviewing
- iFM 2023: 18th International Conference on integrated Formal Methods
- CSL 2023: 31st EACSL Annual Conference on Computer Science Logic
- QPL 2022: 19th International Conference on Quantum Physics and Logic
- ESA 2021: 29th Annual European Symposium on Algorithms
- ICTAC 2020: 17th International Colloquium on Theoretical Aspects of Computing
- CONCUR 2020: 31st International Conference on Concurrency Theory
- CLEI 2019: XLV Latin American Computing Conference
- ICDT 2019: 22nd International Conference on Database Theory
- TACAS 2019: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
- ISWC 2019: 18th International Semantic Web Conference
- LPAR 2017: 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
- ICALP 2016: 43rd International Colloquium on Automata, Languages, and Programming
- FM 2016: 21st International Symposium on Formal Methods
- FORMATS 2015: 13th International Conference on Formal Modeling and Analysis of Timed Systems
- CAV 2015: 27th International Conference on Computer Aided Verification
- CAV 2014: 26th International Conference on Computer Aided Verification
- CSF 2014: 27th IEEE Computer Security Foundations Symposium
- CSF 2013: 26th IEEE Computer Security Foundations Symposium
- MFCS 2012: 37th International Symposium on Mathematical Foundations of Computer Science
- LOPSTR 2010: 20th International Symposium on Logic‑based Program Synthesis and Transformation
- NFM 2010: 2nd NASA Formal Methods Symposium
Journal External Reviewing
Tools
I contributed in the development of the following tools:
- CertiCrypt. CertiCrypt is a framework built on top of the Coq proof assistant that enables the machine-checked construction and verification of language-based cryptographic proofs. It has been successfully used to prove the security of several emblematic cryptographic constructions, including encryption schemes, digital signature schemes, zero-knowledge protocols and hash functions.
- CertiPriv. CertiPriv is a framework built as an extension of CertiCrypt aimed at verifying differential privacy properties of probabilistic programs. Differential privacy is the most robust and widely accepted privacy policy for mining senstitive data. The CertiPriv framework was used to certify privacy properties of several basic (numeric) mechanisms and combinatorial optimization algorithms.
Courses
| 2017 – Present | University of Chile, Chile |
|
|
| 2014 – 2017 | RTWH Aachen University, Germany |
| 2004 – 2008 | National University of Rosario, Argentina |
|
Supervision
Current students
- Ismael Correa, “Metric predicate transformer semantics”, Master thesis
- Martín Segur, “Verificación formal de programas sobre bases de datos probabilísticas”, Master thesis
- Nicolás Brandstetter, “FALAA: Framework para la abstracción de arquitecturas de agentes del lenguaje”, Master thesis (co-supervisor)
- Arturo Kullmer, “Manteniendo la privacidad en los censos nacionales”, Master thesis (co-supervisor)
- Felix Melo, “Synthetic Spanish medical text generation using differential Privacy”, Master thesis (co-supervisor)
- Obriel Muga, “Mejoras al módulo de estadísticas de Easycancha mediante lenguaje natural y herramientas de visualización”, Master thesis in IT
- Francisco Humeres, “Simulando la fluctuación: Pronóstico de adopción, precios y su volatilidad para tarjetas gráficas”, Master thesis in IT (co-supervisor)
- Jonnathan Stevens, “Desarrollo de un intérprete para un lenguaje gradual probabilístico”, Undergrad. engineering project (co-supervisor)
Former students
- Tomás Rivas, “Detección de vulnerabilidades de privacidad en la publicación de datos por parte de instituciones públicas”, Undergrad. engineering project, 2025
- Marcelo Navarro, “Slicing of probabilistic programs based on specifications”, Master thesis, 2025
- Bruno Rodríguez, “Sinopsis privadas para algoritmos de clustering sobre datos dispersos”, Undergrad. engineering project, 2024
- Rodrigo Montoya A., “Automatización de planificación para huertas orgánicas”, Undergrad. engineering project, 2023
- Vicente Reyes, “Estudio e implementación de un lenguaje de autorización para bases de datos relacionales”, Undergrad. engineering project, 2023
- Luis Pinochet G., “Automatización del análisis del tiempo de ejecución de programas probabilísticos”, Undergrad. engineering project, 2022
- Gianluca Carboni M., “Planificador de compras colaborativas”, Undergrad. engineering project, 2021
- Álvaro Yáñez M., “Desarrollo de una herramienta para la calendarización de evaluaciones universitarias”, Undergrad. engineering project, 2020
Short Bio
I have been an assistant professor since June 2017 in the Computer Science Department at the University of Chile. There, I
teach different courses and I am primarily involved in research activities. Before joining the University of Chile, I spent three years as a postdoctoral researcher in the Modeling and Verification Group at the RTWH Aachen University, Germany, and in 2014 I earned my PhD degree from the Technical University of Madrid, Spain. I was born and raised in Argentina, where I obtained my undergraduate degree in computer science from the National University of Rosario.