research
∙
02/03/2023
CheckedCBox: Type Directed Program Partitioning with Checked C for Incremental Spatial Memory Safety
Spatial memory safety violation is still a major issue for C programs. C...
share
research
∙
11/11/2022
Quantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification
Many quantum programs are assured by formal verification, but such verif...
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
∙
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/2020
Proving Quantum Programs Correct
As quantum computing steadily progresses from theory to practice, progra...
research
∙
02/19/2018