| Baldur: Whole-Proof Generation and Repair with Large Language Models E First, MN Rabe, T Ringer, Y Brun ESEC/FSE, 2023 | 258 | 2023 |
| QED at Large: A Survey of Engineering of Formally Verified Software T Ringer, K Palmskog, I Sergey, M Gligoric, Z Tatlock Foundations and Trends® in Programming Languages 5 (2-3), 102-281, 2019 | 124 | 2019 |
| Adapting proof automation to adapt proofs T Ringer, N Yazdani, J Leo, D Grossman Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018 | 52 | 2018 |
| Audacious: User-driven access control with unmodified operating systems T Ringer, D Grossman, F Roesner Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications …, 2016 | 49 | 2016 |
| Passport: Improving Automated Formal Verification Using Identifiers A Sanchez-Stern, E First, T Zhou, Z Kaufman, Y Brun, T Ringer TOPLAS 45 (2), No. 12, pp. 1-30, 2023 | 46 | 2023 |
| Proof Repair Across Type Equivalences T Ringer, RD Porter, N Yazdani, J Leo, D Grossman Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language …, 2021 | 45 | 2021 |
| Proof Repair T Ringer University of Washington, 2021 | 43 | 2021 |
| Transformer-based models are not yet perfect at learning to emulate structural recursion D Zhang, C Tigges, Z Zhang, S Biderman, M Raginsky, T Ringer Transactions on Machine Learning Research, 2024 | 41* | 2024 |
| REPLica: REPL Instrumentation for Coq Analysis T Ringer, A Sanchez-Stern, D Grossman, S Lerner Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 31 | 2020 |
| Ornaments for proof reuse in Coq T Ringer, N Yazdani, J Leo, D Grossman 10th International Conference on Interactive Theorem Proving (ITP 2019), 26 …, 2019 | 29 | 2019 |
| Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset T Reichel, RW Henderson, A Touchet, A Gardner, T Ringer ITP, 2023 | 19 | 2023 |
| Position: Stop treating 'AGI' as the north-star goal of AI research B Blili-Hamelin, C Graziul, L Hancox-Li, H Hazan, EM El-Mhamdi, ... ICML (Position Track), 2025 | 17* | 2025 |
| A solver-aided language for test input generation T Ringer, D Grossman, D Schwartz-Narbonne, S Tasiran Proceedings of the ACM on Programming Languages 1 (OOPSLA), 1-24, 2017 | 17 | 2017 |
| Getting More out of Large Language Models for Proofs SD Zhang, T Ringer, E First AI for Theorem Proving, 2023 | 15 | 2023 |
| Proofster: Automated formal verification A Agrawal, E First, Z Kaufman, T Reichel, S Zhang, T Zhou, ... 2023 IEEE/ACM 45th International Conference on Software Engineering …, 2023 | 11 | 2023 |
| QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning A Sanchez-Stern, A Varghese, Z Kaufman, D Zhang, T Ringer, Y Brun ICSE, 2025 | 9 | 2025 |
| Cobblestone: Iterative Automation for Formal Verification SR Kasibatla, A Agarwal, Y Brun, S Lerner, T Ringer, E First ICSE, 2026 | 2 | 2026 |
| HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement J Hu, J Zhang, Y Zhao, T Ringer arXiv preprint arXiv:2505.15740, 2025 | 2 | 2025 |
| Proof Repair across Quotient Type Equivalences C Viola, M Fan, T Ringer OOPSLA, 2025 | 1 | 2025 |
| ProofDB: A prototype natural language Coq search engine T Reichel, T Ringer 9th Conference on Artificial Intelligence and Theorem Proving (AITP), 2024 | 1 | 2024 |
Emily FirstUniversity of Massachusetts AmherstVerified email at cs.umass.edu
