111 citations · 383 across the 23 of their papers we have counts for
5 papers · 1 filter
Fat Pointers for Temporal Memory Safety of C
Jie Zhou, John Criswell, Michael Hicks
Temporal memory safety bugs, especially use-after-free and double free bugs, pose a major security threat to C programs. Real-world exploits utilizing these bugs enable attackers t…
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…
C to Checked C by 3C
Aravind Machiry, John Kastner, Matt McCutchen +3
Owing to the continued use of C (and C++), spatial safety violations (e.g., buffer overflows) still constitute one of today's most dangerous and prevalent security vulnerabilities.…
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…