30 citations · 55 across the 6 of their papers we have counts for
8 papers
CheckedCBox: Type Directed Program Partitioning with Checked C for Incremental Spatial Memory Safety
Liyi Li, Arunkumar Bhattar, Le Chang +2
Spatial memory safety violation is still a major issue for C programs. Checked-C is a safe dialect of C and extends it with Checked pointer types and annotations that guarantee spa…
Qafny: A Quantum-Program Verifier
Liyi Li, Mingwei Zhu, Rance Cleaveland +4
Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specificati…
A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm
Yuxiang Peng, Kesha Hietala, Runzhou Tao +4
Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but these are only useful if computed answers are correct. While hardware-level…
Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
Finn Voichick, Liyi Li, Robert Rand +1
We introduce Qunity, a new quantum programming language designed to treat quantum computing as a natural generalization of classical computing. Qunity presents a unified syntax whe…
A Formal Model of Checked C
Liyi Li, Yiyun Liu, Deena L. Postol +3
We present a formal model of Checked C, a dialect of C that aims to enforce spatial memory safety. Our model pays particular attention to the semantics of dynamically sized, potent…
Verified Compilation of Quantum Oracles
Liyi Li, Finn Voichick, Kesha Hietala +3
Quantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these so-called oracles are often the l…
Proving Quantum Programs Correct
Kesha Hietala, Robert Rand, Shih-Han Hung +2
As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? Thi…
A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras
Liyi Li, Elsa Gunter
Order-sorted algebras and many sorted algebras exist in a long history with many different implementations and applications. A lot of language specifications have been defined in o…