research
∙
02/20/2023
Symphony: Expressive Secure Multiparty Computation with Coordination
Context: Secure Multiparty Computation (MPC) refers to a family of crypt...
share
research
∙
08/27/2022
Fat Pointers for Temporal Memory Safety of C
Temporal memory safety bugs, especially use-after-free and double free b...
research
∙
04/26/2022
Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
We introduce Qunity, a new quantum programming language designed to trea...
research
∙
04/14/2022
A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm
Quantum computing technology may soon deliver revolutionary improvements...
research
∙
03/25/2022
C to Checked C by 3C
Owing to the continued use of C (and C++), spatial safety violations (e....
research
∙
01/31/2022
A Formal Model of Checked C
We present a formal model of Checked C, a dialect of C that aims to enfo...
research
∙
12/13/2021
Verified Compilation of Quantum Oracles
Quantum algorithms often apply classical operations, such as arithmetic ...
research
∙
10/03/2021
Garbage Collection Makes Rust Easier to Use: A Randomized Controlled Trial of the Bronze Garbage Collector
Rust is a general-purpose programming language that is both type- and me...
research
∙
10/03/2020
Proving Quantum Programs Correct
As quantum computing steadily progresses from theory to practice, progra...
research
∙
12/04/2019
A Verified Optimizer for Quantum Circuits
We present VOQC, the first fully verified compiler for quantum circuits,...
research
∙
07/02/2019
Build It, Break It, Fix It: Contesting Secure Development
Typical security contests focus on breaking or mitigating the impact of ...
research
∙
04/12/2019
Verified Optimization in a Quantum Intermediate Representation
We present sqire, a low-level language for quantum computing and verific...
research
∙
03/28/2019
A Counterexample-guided Approach to Finding Numerical Invariants
Numerical invariants, e.g., relationships among numerical variables in a...
research
∙
01/23/2019
LWeb: Information Flow Security for Multi-tier Web Applications
This paper presents LWeb, a framework for enforcing label-based, informa...
research
∙
11/08/2018
Quantitative Robustness Analysis of Quantum Programs (Extended Version)
Quantum computation is a topic of significant recent interest, with prac...
research
∙
08/29/2018
Evaluating Fuzz Testing
Fuzz testing has enjoyed great success at discovering security critical ...
research
∙
02/24/2018
Evaluating Design Tradeoffs in Numeric Static Analysis for Java
Numeric static analysis for Java has a broad range of potentially useful...
research
∙
02/22/2018
What's the Over/Under? Probabilistic Bounds on Information Leakage
Quantitative information flow (QIF) is concerned with measuring how much...
research
∙
11/25/2017
A Language for Probabilistically Oblivious Computation
An oblivious computation is one that is free of direct and indirect info...
research
∙
11/17/2017