Paper Accepted by OOPSLA 2026

Our paper has been unconditionally accepted for presentation at OOPSLA 2026.

Our paper titled “A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs” by Zhongyi Wang, Tengjie Lin, Mingshuai Chen, Haokun Li (Fermat Labs, Huawei Inc.), Mingqi Yang, Xiao Yi, Shengchao Qin (Fermat Labs, Huawei Inc.), Yixing Luo, Xiaofeng Li, Bin Gu (Beijing Institute of Control Engineering), Liqiang Lu, and Jianwei Yin has been accepted for publication OOPSLA 2026, in Oakland, California, United States, as part of the Proceedings of the ACM on Programming Languages (PACMPL). This article presents Preguss – a modular, fine-grained framework for inferring formal specifications that integrates static analysis and deductive verification in a sound and terminating manner. Preguss is, to the best of our knowledge, the first automated method capable of proving RTE-freeness of real-world programs with over 1,000 LoC (with marginal human effort).