About

Marco Gaboardi is a Professor in the Computer Science department at Boston University, with a Ph.D. in Computer Science from Torino and Nancy. His research focuses on Programming Languages, Formal Methods, and Differential Privacy. He is actively involved in the Principles of Programming and Verification (POPV) group and the Boston-area Data Privacy groups. In addition to his academic role, he serves as Chief Scientist at DPella. Throughout his career, Gaboardi has contributed to advancing formal reasoning in security and privacy, as well as the development of programming tools for adaptive data analysis and formal verification techniques. His academic journey includes positions as Assistant and Associate Professor at Boston University, Assistant Professor at the University at Buffalo, and visiting scholar roles at institutions such as Simons@Berkeley and Harvard CRCS. He has also held fellowships and postdoctoral positions in Europe, including at Dundee, Bologna, and Paris 13. Gaboardi's teaching portfolio includes courses on combinatoric structures, formal methods in security and privacy, and concepts of programming languages, reflecting his commitment to education in foundational and applied aspects of computer science.

Research topics

• Computer Science
• Computer Security
• Programming language
• Mathematics
• Artificial Intelligence
• Internet privacy
• Operations research
• Algorithm
• Arithmetic
• Discrete mathematics
• Theoretical computer science

Selected publications

• A Category-Theoretic Framework for Dependent Effect Systems

  Lecture notes in computer science · 2026-01-01

  book-chapter
  PublisherDOI

• Efficient Decision Procedures for Variants of GKAT (Artifact)

  Zenodo (CERN European Organization for Nuclear Research) · 2026-01-19

  otherOpen accessSenior author

  ESOP 2026 Artifact for #94 Efficient Decision Procedures for Variants of GKAT This repository contains the artifact for the paper: “Efficient Decision Procedures for Variants of GKAT”. Getting Started Included in the Artifact The artifact includes the source code for the following programs: sym-gkat : Our implementation of on-the-fly symbolic GKAT. sym-cf-gkat: Our implementation of on-the-fly symbolic CF-GKAT. cf-gkat : CF-GKAT by Zhang et al.1 (prior work for benchmarking). sym-kat : Sym-KAT by Pous2 (prior work for benchmarking). We include benchmarks extracted from GNU Coreutils (via blinding) as well as synthetic benchmarks created through random generation. These are located in the benchmarks directory. Disclaimer: Very minor modifications are done to cf-gkat and sym-kat to ensure compatibility with our benchmark input format and to report diagnostic information. These modifications do not affect the core algorithms of the original implementations. Docker Image The artifact is packaged as a Docker image for easy reproducibility (tested on docker version 29.1.3). The image is built to support both AMD64 and ARM64 architectures. esop2026-artifact-amd64.tar: for AMD64 architecture esop2026-artifact-arm64.tar: for ARM64 architecture Alternatively, you can build the Docker image from source by following the instructions in the Building from Source section. Loading the Docker Image To load the Docker image, use the following command: docker load -i esop2026-artifact-amd64.tar # for AMD64 architecture or docker load -i esop2026-artifact-arm64.tar # for ARM64 architecture Verify that the Image Loaded Correctly (Optional) To verify that the Docker image has been loaded correctly, you can run the following simple tests for each program: Verify sym-cf-gkat: docker run --rm --entrypoint ./sym-cf-gkat.exe -v ./benchmarks/:/benchmarks/ esop2026-artifact /benchmarks/coreutils/inputs/basename-blind@main.c /benchmarks/coreutils/inputs/basename-decompiled@main.c This command uses sym-cf-gkat to check the equivalence of the blinded and decompiled versions of the main function from the basename program of Coreutils. It should print a JSON output indicating the equivalence result. See the Coreutils Benchmark Results section for an example output. Verify sym-gkat: docker run --rm --entrypoint ./sym-gkat.exe -v ./benchmarks/:/benchmarks/ esop2026-artifact /benchmarks/synthetic/inputs-sexpr/e50b20p50eq/e50b20p50eq_00.txt This command uses sym-gkat to check the equivalence of a pair of equivalent expressions from the synthetic benchmark e50b20p50eq_00.txt. It should print two lines of output indicating the expected equivalence and the decision result as follows: equiv_expected = true equiv_result = true Important: To ensure that the Docker image functions correctly when benchmarking cf-gkat and sym-kat, we recommend allowing Docker to use at least 12 GB of memory and 4 CPUs. Step-by-step Instructions Coreutils The Coreutils benchmarks are applicable to the following programs: - sym-cf-gkat - cf-gkat Coreutil inputs are located in benchmarks/coreutils/inputs. These benchmark inputs are blinded GNU Coreutil programs and their decompiled versions from Ghidra. They follow the naming convention <program>-blind@<function>.c for blinded programs and <program>-decompiled@<function>.c for decompiled versions. Node: The scripts contained in benchmarks/coreutils/scripts are included in the Docker image and should be executed using docker run commands. Running Coreutils Benchmarks The benchmark scripts assume that the benchmarks directory is mounted to /benchmarks/ in the Docker container. Benchmark sym-cf-gkat using BDD backend: docker run --rm --entrypoint ./coreutils/scripts/benchmark_sym_cf_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 7s to complete. Benchmark sym-cf-gkat using SAT backend: docker run --rm --entrypoint ./coreutils/scripts/benchmark_sym_cf_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 7s to complete. Benchmark cf-gkat (slow): docker run --rm --entrypoint ./coreutils/scripts/benchmark_cf_gkat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 40 minutes to complete. The plotting script in the analysis section below does not require the full set of cf-gkat data points to function correctly. Coreutils Benchmark Results Benchmark results will be saved in the respective output directories: - sym-cf-gkat with BDD: benchmarks/coreutils/outputs-sym-cf-gkat-bdd - sym-cf-gkat with SAT: benchmarks/coreutils/outputs-sym-cf-gkat-sat - cf-gkat: benchmarks/coreutils/outputs-cf-gkat The output format of sym-cf-gkat is JSON, as shown in the example below: { "results": [ { "name": "cat", "location1": "./benchmarks/coreutils/inputs/cat-decompiled@cat.c:7:6:80", "location2": "./benchmarks/coreutils/inputs/cat-blind@cat.c:7:6:80", "num_bvars1": 42, "num_bvars2": 42, "num_actions1": 58, "num_actions2": 58, "is_equiv": true, "duration": 584 } ], "diff": [], "duration": 11815 } results: An array of results for each function checked. name: The name of the function. location1 and location2: The file locations of the two checked CF-GKAT expressions. num_bvars1 and num_bvars2: The number of tests in each expression. num_actions1 and num_actions2: The number of actions in each expression. is_equiv: A boolean indicating whether the two expressions are equivalent. duration: The time taken (in microseconds) to check the equivalence of this function. diff: An array containing differences if the expressions are not equivalent. duration: The total time taken (in microseconds) for the checker. The output format of cf-gkat is also JSON, as shown in the example below: {"results":[{"name":"main","is_equiv":["Done",true],"duration":1820.0874328613281}],"duration":39803.98178100586} results: An array of results for each function checked. name: The name of the function. is_equiv: Completion status of the function check.Status could be due to Done(bool): successfully checked equivalence (true/false), Unsupported: unsupported control-flow constructs, Timeout: timeout after 2 minutes, OutOfMemory: out of memory with 4GB limit, Failed: other internal errors duration: The time taken (in microseconds) to check the equivalence of this function. duration: The total time taken (in microseconds) for the checker. Analysis of Coreutils Benchmark Results To analyze and plot the benchmark results, use the following command: docker run --rm --entrypoint ./coreutils/scripts/plot_logs.py -v ./benchmarks:/benchmarks/ esop2026-artifact The docker container already has all the required dependencies installed to run the script. All of the necessary log files will be read from the output directories mentioned above. This will generate scatter plots for time and memory usage comparisons between the different tools. The plotting script with create a new directory benchmarks/coreutils/analysis and save the generated plots there. Synthetic Benchmarks The synthetic benchmarks are applicable to the following programs: - sym-gkat - sym-cf-gkat - cf-gkat (limited set due to scalability issues) - sym-kat The synthetic benchmarks are generated randomly with varying parameters such as the number of actions, number of tests, and expression depth. Each benchmark consists of 100 pairs of expressions to be checked for equivalence. For instance, the benchmark e50b20p50eq contains 100 pairs of expressions where each expression has approximately 50 structural connectives (prefix e50), a maximum of 20 unique boolean variables (prefix b20) per test, and a maximum of 50 primitive actions (prefix p50). The suffix eq indicates that the pairs of expressions are equivalent. The synthetic benchmarks come in two different formats: 1. .c files: These files contain C code that can be used as inputs to sym-cf-gkat and cf-gkat. These files are located in benchmarks/synthetic/inputs-cexpr. 2. .txt files: These files contain KAT expressions in S-expression format that can be used as inputs to sym-gkat and sym-kat. These files are located in benchmarks/synthetic/inputs-sexpr. The benchmarks using these two formats are equivalent. Running Synthetic Benchmarks The benchmark scripts assume that the benchmarks directory is mounted to /benchmarks/ in the Docker container. Benchmark sym-gkat using BDD backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 80s to complete. Benchmark sym-gkat using SAT backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 30s to complete. Benchmark sym-cf-gkat using BDD backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_cf_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 140s to complete. Benchmark sym-cf-gkat using SAT backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_cf_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 140s to complete. Benchmark sym-kat (slow): docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_kat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 3.5h to complete. The plotting script in the analysis section below does not require the full set of sym-kat data points to function correctly. Benchmark cf-gkat (very slow): docker run --rm --entrypoint ./synthetic/scripts/benchmark_cf_gkat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: Due the scalability limitation of the original cf-

  PublisherDOI

• Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT

  Lecture notes in computer science · 2026-01-01

  book-chapterSenior author
  PublisherDOI

• Efficient Decision Procedures for Variants of GKAT (Artifact)

  Zenodo (CERN European Organization for Nuclear Research) · 2026-01-02

  otherOpen accessSenior author

  ESOP 2026 Artifact for #94 Efficient Decision Procedures for Variants of GKAT This repository contains the artifact for the paper: “Efficient Decision Procedures for Variants of GKAT”. Getting Started Included in the Artifact The artifact includes the source code for the following programs: sym-gkat : Our implementation of on-the-fly symbolic GKAT. sym-cf-gkat: Our implementation of on-the-fly symbolic CF-GKAT. cf-gkat : CF-GKAT by Zhang et al.1 (prior work for benchmarking). sym-kat : Sym-KAT by Pous2 (prior work for benchmarking). We include benchmarks extracted from GNU Coreutils (via blinding) as well as synthetic benchmarks created through random generation. These are located in the benchmarks directory. Disclaimer: Very minor modifications are done to cf-gkat and sym-kat to ensure compatibility with our benchmark input format and to report diagnostic information. These modifications do not affect the core algorithms of the original implementations. Docker Image The artifact is packaged as a Docker image for easy reproducibility. The image is built to support both AMD64 and ARM64 architectures. Alternatively, you can build the Docker image from source by following the instructions in the Building from Source section. Loading the Docker Image To load the Docker image, use the following command, replacing <path-to-image> with the path to the appropriate tar file for your architecture: docker load -i <path-to-image> Verify that the Image Loaded Correctly (Optional) To verify that the Docker image has been loaded correctly, you can run the following simple tests for each program: Verify sym-cf-gkat: docker run --rm --entrypoint ./sym-cf-gkat.exe -v ./benchmarks/:/benchmarks/ esop2026-artifact /benchmarks/coreutils/inputs/basename-blind@main.c /benchmarks/coreutils/inputs/basename-decompiled@main.c This command uses sym-cf-gkat to check the equivalence of the blinded and decompiled versions of the main function from the basename program of Coreutils. It should print a JSON output indicating the equivalence result. Verify sym-gkat: docker run --rm --entrypoint ./sym-gkat.exe -v ./benchmarks/:/benchmarks/ esop2026-artifact /benchmarks/synthetic/inputs-sexpr/e50b20p50eq/e50b20p50eq_00.txt This command uses sym-gkat to check the equivalence of a pair of equivalent expressions from the synthetic benchmark e50b20p50eq_00.txt. It should print two lines of output indicating the expected equivalence and the decision result. Important: To ensure that the Docker image functions correctly when benchmarking cf-gkat and sym-kat, we recommend allowing Docker to use at least 12 GB of memory and 4 CPUs. Step-by-step Instructions Coreutils The Coreutils benchmarks are applicable to the following programs: - sym-cf-gkat - cf-gkat Coreutil inputs are located in benchmarks/coreutils/inputs. These benchmark inputs are blinded GNU Coreutil programs and their decompiled versions from Ghidra. They follow the naming convention <program>-blind@<function>.c for blinded programs and <program>-decompiled@<function>.c for decompiled versions. Node: The scripts contained in benchmarks/coreutils/scripts are included in the Docker image and should be executed using docker run commands. Running Coreutils Benchmarks The benchmark scripts assume that the benchmarks directory is mounted to /benchmarks/ in the Docker container. Benchmark sym-cf-gkat using BDD backend: docker run --rm --entrypoint ./coreutils/scripts/benchmark_sym_cf_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 7s to complete. Benchmark sym-cf-gkat using SAT backend: docker run --rm --entrypoint ./coreutils/scripts/benchmark_sym_cf_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 7s to complete. Benchmark cf-gkat (slow): docker run --rm --entrypoint ./coreutils/scripts/benchmark_cf_gkat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 40 minutes to complete. The plotting script in the analysis section below does not require the full set of cf-gkat data points to function correctly. Coreutils Benchmark Results Benchmark results will be saved in the respective output directories: - sym-cf-gkat with BDD: benchmarks/coreutils/outputs-sym-cf-gkat-bdd - sym-cf-gkat with SAT: benchmarks/coreutils/outputs-sym-cf-gkat-sat - cf-gkat: benchmarks/coreutils/outputs-cf-gkat The output format of sym-cf-gkat is JSON, as shown in the example below: { "results": [ { "name": "cat", "location1": "./benchmarks/coreutils/inputs/cat-decompiled@cat.c:7:6:80", "location2": "./benchmarks/coreutils/inputs/cat-blind@cat.c:7:6:80", "num_bvars1": 42, "num_bvars2": 42, "num_actions1": 58, "num_actions2": 58, "is_equiv": true, "duration": 584 } ], "diff": [], "duration": 11815 } results: An array of results for each function checked. name: The name of the function. location1 and location2: The file locations of the two checked CF-GKAT expressions. num_bvars1 and num_bvars2: The number of tests in each expression. num_actions1 and num_actions2: The number of actions in each expression. is_equiv: A boolean indicating whether the two expressions are equivalent. duration: The time taken (in microseconds) to check the equivalence of this function. diff: An array containing differences if the expressions are not equivalent. duration: The total time taken (in microseconds) for the checker. The output format of cf-gkat is also JSON, as shown in the example below: {"results":[{"name":"main","is_equiv":["Done",true],"duration":1820.0874328613281}],"duration":39803.98178100586} results: An array of results for each function checked. name: The name of the function. is_equiv: Completion status of the function check.Status could be due to Done(bool): successfully checked equivalence (true/false), Unsupported: unsupported control-flow constructs, Timeout: timeout after 2 minutes, OutOfMemory: out of memory with 4GB limit, Failed: other internal errors duration: The time taken (in microseconds) to check the equivalence of this function. duration: The total time taken (in microseconds) for the checker. Analysis of Coreutils Benchmark Results To analyze and plot the benchmark results, use the following command: docker run --rm --entrypoint ./coreutils/scripts/plot_logs.py -v ./benchmarks:/benchmarks/ esop2026-artifact The docker container already has all the required dependencies installed to run the script. All of the necessary log files will be read from the output directories mentioned above. This will generate scatter plots for time and memory usage comparisons between the different tools. The plots will be saved in the benchmarks/coreutils/analysis directory. Synthetic Benchmarks The synthetic benchmarks are applicable to the following programs: - sym-gkat - sym-cf-gkat - cf-gkat (limited set due to scalability issues) - sym-kat The synthetic benchmarks are generated randomly with varying parameters such as the number of actions, number of tests, and expression depth. Each benchmark consists of 100 pairs of expressions to be checked for equivalence. For instance, the benchmark e50b20p50eq contains 100 pairs of expressions where each expression has approximately 50 structural connectives (prefix e50), a maximum of 20 unique boolean variables (prefix b20) per test, and a maximum of 50 primitive actions (prefix p50). The suffix eq indicates that the pairs of expressions are equivalent. The synthetic benchmarks come in two different formats: 1. .c files: These files contain C code that can be used as inputs to sym-cf-gkat and cf-gkat. These files are located in benchmarks/synthetic/inputs-cexpr. 2. .txt files: These files contain KAT expressions in S-expression format that can be used as inputs to sym-gkat and sym-kat. These files are located in benchmarks/synthetic/inputs-sexpr. The benchmarks using these two formats are equivalent. Running Synthetic Benchmarks The benchmark scripts assume that the benchmarks directory is mounted to /benchmarks/ in the Docker container. Benchmark sym-gkat using BDD backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 80s to complete. Benchmark sym-gkat using SAT backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 30s to complete. Benchmark sym-cf-gkat using BDD backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_cf_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 140s to complete. Benchmark sym-cf-gkat using SAT backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_cf_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 140s to complete. Benchmark sym-kat (slow): docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_kat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 3.5h to complete. The plotting script in the analysis section below does not require the full set of sym-kat data points to function correctly. Benchmark cf-gkat (very slow): docker run --rm --entrypoint ./synthetic/scripts/benchmark_cf_gkat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: Due the scalability limitation of the original cf-gkat algorithm3, we do not expect it to complete the full set of synthetic benchmarks within a reasonable time frame. For this reason, its data points are not required or used by the analysis scripts below. Synthetic Benchmark Results The benchmark results will be saved in respective log files in the benchmarks/synthetic/logs

  PublisherDOI

• Cryptis: Cryptographic Reasoning in Separation Logic

  Proceedings of the ACM on Programming Languages · 2026-01-08

  articleOpen accessSenior author

  We introduce Cryptis, an extension of the Iris separation logic for the symbolic model of cryptography. The combination of separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol. To make this integration possible, we propose novel specifications for authentication protocols that allow agents in a network to agree on the use of system resources. We evaluate our approach by verifying various authentication protocols and a key-value store server that uses these authentication protocols to connect to clients. Our results are formalized in Rocq.

  PublisherDOI

• Cryptis: Cryptographic Reasoning in Separation Logic

  ArXiv.org · 2025-02-28

  preprintOpen accessSenior author

  We introduce Cryptis, an extension of the Iris separation logic that can be used to verify cryptographic components using the symbolic model of cryptography. The combination of separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol. To make this integration possible, we propose novel specifications for authentication protocols that allow agents in a network to agree on the use of system resources. We evaluate our approach by verifying various authentication protocols and a key-value store server that uses these authentication protocols to connect to clients. Our results are formalized in Coq.

  PublisherOA PDFDOI

• BiGKAT: An Algebraic Framework for Relational Verification of Probabilistic Programs

  Lecture notes in computer science · 2025-01-01 · 2 citations

  book-chapterOpen accessSenior author

  Abstract This work is devoted to formal reasoning on relational properties of probabilistic imperative programs. Relational properties are properties which relate the execution of two programs (possibly the same one) on two initial memories. We aim at extending the algebraic approach of Kleene Algebras with Tests (KAT) to relational properties of probabilistic programs. For that we consider the approach of Guarded Kleene Algebras with Tests (GKAT), which can be used for representing probabilistic programs, and define a relational version of it, called Bi-guarded Kleene Algebras with Tests (BiGKAT) together with a semantics. We show that the setting of BiGKAT is expressive enough to encode a finitary version of probabilistic Relational Hoare Logic (pRHL) (without the While rule), a program logic that has been introduced in the literature for the verification of relational properties of probabilistic programs. We also discuss the additional expressivity brought by BiGKAT.

  PublisherOA PDFDOI

• Efficient Decision Procedures for Variants of GKAT (Artifact)

  Zenodo (CERN European Organization for Nuclear Research) · 2025-12-31

  otherOpen accessSenior author

  ESOP 2026 Artifact for #94 Efficient Decision Procedures for Variants of GKAT This repository contains the artifact for the paper: “Efficient Decision Procedures for Variants of GKAT”. Getting Started Included in the Artifact The artifact includes the source code for the following programs: sym-gkat : Our implementation of on-the-fly symbolic GKAT. sym-cf-gkat: Our implementation of on-the-fly symbolic CF-GKAT. cf-gkat : CF-GKAT by Zhang et al.1 (prior work for benchmarking). sym-kat : Sym-KAT by Pous2 (prior work for benchmarking). We include benchmarks extracted from GNU Coreutils (via blinding) as well as synthetic benchmarks created through random generation. These are located in the benchmarks directory. Disclaimer: Very minor modifications are done to cf-gkat and sym-kat to ensure compatibility with our benchmark input format and to report diagnostic information. These modifications do not affect the core algorithms of the original implementations. Docker Image The artifact is packaged as a Docker image for easy reproducibility. The image is built to support both AMD64 and ARM64 architectures. Alternatively, you can build the Docker image from source by following the instructions in the Building from Source section. Loading the Docker Image To load the Docker image, use the following command, replacing <path-to-image> with the path to the appropriate tar file for your architecture: docker load -i <path-to-image> Verify that the Image Loaded Correctly (Optional) To verify that the Docker image has been loaded correctly, you can run the following simple tests for each program: Verify sym-cf-gkat: docker run --rm --entrypoint ./sym-cf-gkat.exe -v ./benchmarks/:/benchmarks/ esop2026-artifact /benchmarks/coreutils/inputs/basename-blind@main.c /benchmarks/coreutils/inputs/basename-decompiled@main.c This command uses sym-cf-gkat to check the equivalence of the blinded and decompiled versions of the main function from the basename program of Coreutils. It should print a JSON output indicating the equivalence result. Verify sym-gkat: docker run --rm --entrypoint ./sym-gkat.exe -v ./benchmarks/:/benchmarks/ esop2026-artifact /benchmarks/synthetic/inputs-sexpr/e50b20p50eq/e50b20p50eq_00.txt This command uses sym-gkat to check the equivalence of a pair of equivalent expressions from the synthetic benchmark e50b20p50eq_00.txt. It should print two lines of output indicating the expected equivalence and the decision result. Important: To ensure that the Docker image functions correctly when benchmarking cf-gkat and sym-kat, we recommend allowing Docker to use at least 12 GB of memory and 4 CPUs. Step-by-step Instructions Coreutils The Coreutils benchmarks are applicable to the following programs: - sym-cf-gkat - cf-gkat Coreutil inputs are located in benchmarks/coreutils/inputs. These benchmark inputs are blinded GNU Coreutil programs and their decompiled versions from Ghidra. They follow the naming convention <program>-blind@<function>.c for blinded programs and <program>-decompiled@<function>.c for decompiled versions. Node: The scripts contained in benchmarks/coreutils/scripts are included in the Docker image and should be executed using docker run commands. Running Coreutils Benchmarks The benchmark scripts assume that the benchmarks directory is mounted to /benchmarks/ in the Docker container. Benchmark sym-cf-gkat using BDD backend: docker run --rm --entrypoint ./coreutils/scripts/benchmark_sym_cf_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 7s to complete. Benchmark sym-cf-gkat using SAT backend: docker run --rm --entrypoint ./coreutils/scripts/benchmark_sym_cf_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 30s to complete (mainly due to a degenerate case copy@copy_internal). Benchmark cf-gkat (slow): docker run --rm --entrypoint ./coreutils/scripts/benchmark_cf_gkat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 40 minutes to complete. The plotting script in the analysis section below does not require the full set of cf-gkat data points to function correctly. Coreutils Benchmark Results Benchmark results will be saved in the respective output directories: - sym-cf-gkat with BDD: benchmarks/coreutils/outputs-sym-cf-gkat-bdd - sym-cf-gkat with SAT: benchmarks/coreutils/outputs-sym-cf-gkat-sat - cf-gkat: benchmarks/coreutils/outputs-cf-gkat The output format of sym-cf-gkat is JSON, as shown in the example below: { "results": [ { "name": "cat", "location1": "./benchmarks/coreutils/inputs/cat-decompiled@cat.c:7:6:80", "location2": "./benchmarks/coreutils/inputs/cat-blind@cat.c:7:6:80", "num_bvars1": 42, "num_bvars2": 42, "num_actions1": 58, "num_actions2": 58, "is_equiv": true, "duration": 584 } ], "diff": [], "duration": 11815 } results: An array of results for each function checked. name: The name of the function. location1 and location2: The file locations of the two checked CF-GKAT expressions. num_bvars1 and num_bvars2: The number of tests in each expression. num_actions1 and num_actions2: The number of actions in each expression. is_equiv: A boolean indicating whether the two expressions are equivalent. duration: The time taken (in microseconds) to check the equivalence of this function. diff: An array containing differences if the expressions are not equivalent. duration: The total time taken (in microseconds) for the checker. The output format of cf-gkat is also JSON, as shown in the example below: {"results":[{"name":"main","is_equiv":["Done",true],"duration":1820.0874328613281}],"duration":39803.98178100586} results: An array of results for each function checked. name: The name of the function. is_equiv: Completion status of the function check.Status could be due to Done(bool): successfully checked equivalence (true/false), Unsupported: unsupported control-flow constructs, Timeout: timeout after 2 minutes, OutOfMemory: out of memory with 4GB limit, Failed: other internal errors duration: The time taken (in microseconds) to check the equivalence of this function. duration: The total time taken (in microseconds) for the checker. Analysis of Coreutils Benchmark Results To analyze and plot the benchmark results, use the following command: docker run --rm --entrypoint ./coreutils/scripts/plot_logs.py -v ./benchmarks:/benchmarks/ esop2026-artifact The docker container already has all the required dependencies installed to run the script. All of the necessary log files will be read from the output directories mentioned above. This will generate scatter plots for time and memory usage comparisons between the different tools. The plots will be saved in the benchmarks/coreutils/analysis directory. Synthetic Benchmarks The synthetic benchmarks are applicable to the following programs: - sym-gkat - sym-cf-gkat - cf-gkat (limited set due to scalability issues) - sym-kat The synthetic benchmarks are generated randomly with varying parameters such as the number of actions, number of tests, and expression depth. Each benchmark consists of 100 pairs of expressions to be checked for equivalence. For instance, the benchmark e50b20p50eq contains 100 pairs of expressions where each expression has approximately 50 structural connectives (prefix e50), a maximum of 20 unique boolean variables (prefix b20) per test, and a maximum of 50 primitive actions (prefix p50). The suffix eq indicates that the pairs of expressions are equivalent. The synthetic benchmarks come in two different formats: 1. .c files: These files contain C code that can be used as inputs to sym-cf-gkat and cf-gkat. These files are located in benchmarks/synthetic/inputs-cexpr. 2. .txt files: These files contain KAT expressions in S-expression format that can be used as inputs to sym-gkat and sym-kat. These files are located in benchmarks/synthetic/inputs-sexpr. The benchmarks using these two formats are equivalent. Running Synthetic Benchmarks The benchmark scripts assume that the benchmarks directory is mounted to /benchmarks/ in the Docker container. Benchmark sym-gkat using BDD backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 80s to complete. Benchmark sym-gkat using SAT backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 30s to complete. Benchmark sym-cf-gkat using BDD backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_cf_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 140s to complete. Benchmark sym-cf-gkat using SAT backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_cf_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 140s to complete. Benchmark sym-kat (slow): docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_kat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 3.5h to complete. The plotting script in the analysis section below does not require the full set of sym-kat data points to function correctly. Benchmark cf-gkat (very slow): docker run --rm --entrypoint ./synthetic/scripts/benchmark_cf_gkat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: Due the scalability limitation of the original cf-gkat algorithm3, we do not expect it to complete the full set of synthetic benchmarks within a reasonable time frame. For this reason, its data points are not required or used by the analysis scripts below. Synthetic Benchmark Results The benchmark results will be saved in

  PublisherDOI

• Accuracy for Differentially Private Quotients by Fractional Uncertainties

  2025-11-19

  articleOpen accessSenior author

  Differential Privacy (DP) is a cornerstone for ensuring privacy in data analysis by injecting carefully calibrated noise into statistical queries. While numerous DP tools focus on privacy protection, few provide accuracy information, specially for data-dependent computations like averages or quotients of DP-sums. This paper introduces a novel approach to compute confidence intervals, i.e., α-β accuracy, for these computations, leveraging principles from uncertainty propagation. Our method identifies conditions under which analytical error can be predicted, revealing two key invariants: the analytical error improves with large dataset sizes, and addition of values with higher variability require larger dataset sizes for accurate estimation. To simplify adoption, we also propose accuracy tuners to enable rapid determination of minimum dataset sizes and explore trade-offs between privacy budgets and the possibility to perform accuracy estimations. Our theoretical contributions are validated through an empirical evaluation that explores the applicability of fractional uncertainties for computing concrete α-β error across diverse scenarios.

  PublisherOA PDFDOI

• Probabilistic Refinement Session Types

  Proceedings of the ACM on Programming Languages · 2025-06-10 · 1 citations

  articleOpen accessSenior author

  Session types provide a formal type system to define and verify communication protocols between message-passing processes. In order to analyze randomized systems, recent works have extended session types with probabilistic type constructors. Unfortunately, all the proposed extensions only support constant probabilities which limits their applicability to real-world systems. Our work addresses this limitation by introducing probabilistic refinement session types which enable symbolic reasoning for concurrent probabilistic systems in a core calculus we call PReST. The type system is carefully designed to be a conservative extension of refinement session types and supports both probabilistic and regular choice type operators. We also implement PReST in a prototype which we use for validating probabilistic concurrent programs. The added expressive power leads to significant challenges, both in the meta theory and implementation of PReST, particularly with type checking: it requires reconstructing intermediate types for channels when type checking probabilistic branching expressions. The theory handles this by semantically quantifying refinement variables in probabilistic typing rules, a deviation from standard refinement type systems. The implementation relies on a bi-directional type checker that uses an SMT solver to reconstruct the intermediate types minimizing annotation overhead and increasing usability. To guarantee that probabilistic processes are almost-surely terminating, we integrate cost analysis into our type system to obtain expected upper bounds on recursion depth. We evaluate PReST on a wide variety of benchmarks from 4 categories: (i) randomized distributed protocols such as Itai and Rodeh's leader election, bounded retransmission, etc., (ii) parametric Markov chains such as random walks, (iii) probabilistic analysis of concurrent data structures such as queues, and (iv) distributions obtained by composing uniform distributions using operators like max, and sum. Our experiments show that the PReST type checker scales to large programs with sophisticated probabilistic distributions.

  PublisherDOI

Recent grants

• SHF: Small: Collaborative Research: Programming Tools for Adaptive Data Analysis

  NSF · $153k · 2020–2021

• CAREER: FormalDP: Formally Verified, Private, Accurate and Efficient Data Analysis

  NSF · $188k · 2019–2020

• SHF: Small: Collaborative Research: Programming Tools for Adaptive Data Analysis

  NSF · $224k · 2017–2020

• TWC: Large: Collaborative: Computing Over Distributed Sensitive Data

  NSF · $528k · 2016–2020

• TWC: Large: Collaborative: Computing Over Distributed Sensitive Data

  NSF · $96k · 2020–2022

Frequent coauthors

• Gilles Barthe

  Max Planck Institute for Security and Privacy

  48 shared

• Justin Hsu

  43 shared

• Deepak Garg

  Max Planck Institute for Software Systems

  27 shared

• Shin-ya Katsumata

  21 shared

• Patrick Baillot

  Université de Lille

  21 shared

• Simona Ronchi Della Rocca

  University of Turin

  18 shared

• Pierre-Yves Strub

  18 shared

• Mark Bun

  15 shared

Labs

• Data Mining & Data ManagementPI

Education

• Ph.D.

  University of Torino and National Polytechnic Institute of Lorraine

  2007

• M.S.

  University of Milano – Bicocca

  2004

• B.S.

  University of Milano – Bicocca

  2002

Awards & honors

• EU Marie Curie Fellowship
• NSF CAREER award