Finding Semantically-Equivalent Binary Code By Synthesizing Adaptors. - Vaibhav Sharma 001; Kesha Hietala; Stephen McCamant (CoRR, 2017)

Finding Substitutable Binary Code for Reverse Engineering by Synthesizing Adapters. - Vaibhav Sharma 001; Kesha Hietala; Stephen McCamant (ICST, 2018)

Volume-Based Merge Heuristics for Disjunctive Numeric Domains. - Andrew Ruef; Kesha Hietala; Arlen Cox (SAS, 2018)

Quantitative Robustness Analysis of Quantum Programs (Extended Version). - Shih-Han Hung; Kesha Hietala; Shaopeng Zhu; Mingsheng Ying; Michael Hicks 001; Xiaodi Wu 001 (CoRR, 2018)

Formal Verification vs. Quantum Uncertainty. - Robert Rand 001; Kesha Hietala; Michael Hicks 001 (SNAPL, 2019)

Verified Optimization in a Quantum Intermediate Representation. - Kesha Hietala; Robert Rand 001; Shih-Han Hung; Xiaodi Wu 001; Michael Hicks 001 (CoRR, 2019)

Quantitative robustness analysis of quantum programs. - Shih-Han Hung; Kesha Hietala; Shaopeng Zhu; Mingsheng Ying; Michael Hicks 001; Xiaodi Wu 001 (Proc. ACM Program. Lang., 2019)

Proving Quantum Programs Correct. - Kesha Hietala; Robert Rand 001; Shih-Han Hung; Liyi Li 002; Michael Hicks 001 (ITP, 2021)

A verified optimizer for Quantum circuits. - Kesha Hietala; Robert Rand 001; Shih-Han Hung; Xiaodi Wu 001; Michael Hicks 001 (Proc. ACM Program. Lang., 2021)

Finding Substitutable Binary Code By Synthesizing Adapters. - Vaibhav Sharma 001; Kesha Hietala; Stephen McCamant (IEEE Trans. Software Eng., 2021)

A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm. - Yuxiang Peng; Kesha Hietala; Runzhou Tao; Liyi Li 002; Robert Rand 001; Michael Hicks 001; Xiaodi Wu 001 (CoRR, 2022)

Q# as a Quantum Algorithmic Language. - Kartik Singhal 002; Kesha Hietala; Sarah Marshall; Robert Rand 001 (QPL, 2022)

Verified compilation of Quantum oracles. - Liyi Li 002; Finn Voichick; Kesha Hietala; Yuxiang Peng; Xiaodi Wu 001; Michael Hicks 001 (Proc. ACM Program. Lang., 2022)

A Verified Software Toolchain for Quantum Programming. - Kesha Hietala (2022)

FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores. - Arvind Arasu; Tahina Ramananandro; Aseem Rastogi; Nikhil Swamy; Aymeric Fromherz; Kesha Hietala; Bryan Parno; Ravi Ramamurthy (CPP, 2023)

A Verified Optimizer for Quantum Circuits. - Kesha Hietala; Robert Rand 001; Liyi Li 002; Shih-Han Hung; Xiaodi Wu 001; Michael Hicks 001 (ACM Trans. Program. Lang. Syst., 2023)

How We Built Cedar: A Verification-Guided Approach. - Craig Disselkoen; Aaron Eline; Shaobo He; Kyle Headley; Michael Hicks 001; Kesha Hietala; John H. Kastner; Anwar Mamat; Matt McCutchen; Neha Rungta; Bhakti Shah; Emina Torlak; et al. (SIGSOFT FSE Companion, 2024)

Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version). - Joseph W. Cutler; Craig Disselkoen; Aaron Eline; Shaobo He; Kyle Headley; Michael Hicks 001; Kesha Hietala; Eleftherios Ioannidis; John H. Kastner; Anwar Mamat; Darin McAdams; Matt McCutchen; et al. (CoRR, 2024)

Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. - Joseph W. Cutler; Craig Disselkoen; Aaron Eline; Shaobo He; Kyle Headley; Michael Hicks 001; Kesha Hietala; Eleftherios Ioannidis; John H. Kastner; Anwar Mamat; Darin McAdams; Matt McCutchen; et al. (Proc. ACM Program. Lang., 2024)