Chuyue Sun

16 papers A* 1Journal 10Unranked 5
YearRankTypeTitle / Venue / Authors
2026 — conf
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus.
TACAS (2)
Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill, Clark W. Barrett
2025 — conf
ClassInvGen: Class Invariant Synthesis Using Large Language Models.
SAIV
Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark W. Barrett, David L. Dill, Xiaokang Qiu, Shuvendu K. Lahiri
2025 J jnl
ClassInvGen: Class Invariant Synthesis using Large Language Models.
CoRR
Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark W. Barrett, David L. Dill, Xiaokang Qiu, Shuvendu K. Lahiri
2025 J jnl
DafnyBench: A Benchmark for Formal Software Verification.
Trans. Mach. Learn. Res.
Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, Max Tegmark
2025 — conf
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4.
TACAS (1)
Leni Aniva, Chuyue Sun, Brando Miranda, Clark W. Barrett, Sanmi Koyejo
2025 J jnl
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus.
CoRR
Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill, Clark W. Barrett
2024 — conf
Clover: Closed-Loop Verifiable Code Generation.
SAIV
Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett
2024 J jnl
DafnyBench: A Benchmark for Formal Software Verification.
CoRR
Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, Max Tegmark
2024 J jnl
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4.
CoRR
Leni Aniva, Chuyue Sun, Brando Miranda, Clark W. Barrett, Sanmi Koyejo
2024 A* conf
SGLang: Efficient Execution of Structured Language Model Programs.
NeurIPS
Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Chuyue Sun, Jeff Huang, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark W. Barrett, Ying Sheng
2023 J jnl
Clover: Closed-Loop Verifiable Code Generation.
CoRR
Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett
2023 — conf
CryptOpt: Automatic Optimization of Straightline Code.
ICSE Companion
Joel Kuepper, David Wu, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2023 J jnl
CryptOpt: Automatic Optimization of Straightline Code.
CoRR
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2023 J jnl
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives.
Proc. ACM Program. Lang.
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2023 J jnl
Efficiently Programming Large Language Models using SGLang.
CoRR
Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Jeff Huang, Chuyue Sun, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark W. Barrett, Ying Sheng
2022 J jnl
CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives.
CoRR
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom