Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill, Clark Barrett. VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. Accepted at TACAS 2026. October 2025. [paper] [code] [BibTeX]
Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark Barrett, David Dill, Xiaokang Qiu, Shuvendu K. Lahiri. ClassInvGen: Class Invariant Synthesis Using Large Language Models. The 8th International Symposium on AI Verification (SAIV 2025). [paper] [BibTeX]
Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, Sanmi Koyejo Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 . December 2024. [paper] [BibTeX]
Chloe Loughridge*, Qinyi Sun*, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, Max Tegmark. DafnyBench: A Benchmark for Formal Software Verification. Transactions on Machine Learning Research . December 2024. [paper] [BibTeX]
Chuyue Sun*, Ying Sheng*, Oded Padon, Clark Barrett. Clover: Closed-Loop Verifiable Code Generation. The 7th International Symposium on AI Verification (SAIV'24). June 2024. [paper] [BibTeX]
Lianmin Zheng*, Liangsheng Yin, Zhiqiang Xie, Jeff Huang, Chuyue Sun, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E Gonzalez, Clark Barrett, Ying Sheng*. Efficiently Programming Large Language Models using SGLang. The Thirty-Eighth Annual Conference on Neural Information Processing Systems (NeurIPS'24). December 2024. [paper] [BibTeX]
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom. CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives. Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'23). Distinguished Paper Award. June 2023. [paper] [BibTeX]
Chuyue Sun, Christopher Hahn, Caroline Trippel. Towards Improving Verification Productivity with Circuit-Aware Translation of Natural Language to SystemVerilog Assertions. The First International Workshop on Deep Learning-aided Verification (DAV '23) co-located with the 35th International Conference on Computer-Aided Verification (CAV '23). July 2023. [paper] [BibTeX]
Clover: Closed-Loop Verifiable Code Generation. the 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024) Dafny Workshop, Jan 2024
Towards Improving Verification Productivity with Circuit-Aware Translation of Natural Language to SystemVerilog Assertions. The First International Workshop on Deep Learning-aided Verification (DAV '23) co-located with the 35th International Conference on Computer-Aided Verification (CAV '23), July 2023
Clover: Closed-Loop Verifiable Code Generation. Center for Automated Reasoning at Stanford University (Centuar) Annual Meeting 2023, August 2023