Fetching the paper…
Reading the bibliography…
Generative AI has shown its values for many software engineering tasks.
Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow) . Lecture Notes in Computer Science, Vol. 828
Lawrence C. Paulson. 1994 · 1994
Earlier work this paper cites.
The Coq proof assistant reference manual
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al · 1999
Earlier work this paper cites.
Generative Language Modeling for Automated Theorem Proving
Stanislas Polu and Ilya Sutskever. 2020 · 2009
Earlier work this paper cites.
Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 6355) , Edmund M. Clarke and Andrei Voronkov (Eds.). Springer, 348–370
K. Rustan M. Leino. 2010 · 2010
Earlier work this paper cites.
Dependent types and multi-monadic effects in F. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 , Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 256–270
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. 2016 · 2016
Earlier work this paper cites.
RustBelt: securing the foundations of the rust programming language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018 · 2018
Earlier work this paper cites.
Leveraging rust types for modular specification and verification
Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers. 2019 · 2019
Earlier work this paper cites.
HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA (Proceedings of Machine Learning Research, Vol. 97) . PMLR, 454–463
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. 2019 · 2019
Earlier work this paper cites.
Learning to Prove Theorems via Interacting with Proof Assistants. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA (Proceedings of Machine Learning Research, Vol. 97) . PMLR, 6984–6994
Kaiyu Yang and Jia Deng. 2019 · 2019
Earlier work this paper cites.
TacTok: semantics-aware proof synthesis
Emily First, Yuriy Brun, and Arjun Guha. 2020 · 2020
Earlier work this paper cites.
Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, MAPL@PLDI 2020, London, UK, June 15, 2020 . ACM, 1–10
Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner. 2020 · 2020
Earlier work this paper cites.
Program Synthesis with Large Language Models
Jacob Austin, Augustus Odena, Maxwell I. Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie J. Cai, Michael Terry, Quoc V. Le, and Charles Sutton. 2021 · 2021
Earlier work this paper cites.
Diffy: Inductive Reasoning of Array Programs Using Difference Invariants. In Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 12760) , Alexandra Silva and K. Rustan M. Leino (Eds.). Springer, 911–935
Supratik Chakraborty, Ashutosh Gupta, and Divyesh Unadkat. 2021 · 2021
Earlier work this paper cites.
Evaluating large language models trained on code
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde De Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al · 2021
Earlier work this paper cites.
The Lean 4 Theorem Prover and Programming Language. In Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings (Lecture Notes in Computer Science, Vol. 12699) , André Platzer and Geoff Sutcliffe (Eds.). Springer, 625–635
Leonardo de Moura and Sebastian Ullrich. 2021 · 2021
Earlier work this paper cites.
Houdini, an Annotation Assistant for ESC/Java. In FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings (Lecture Notes in Computer Science, Vol. 2021) , José Nuno Oliveira and Pamela Zave (Eds.). Springer, 500–517
Cormac Flanagan and K. Rustan M. Leino. 2001 · 2021
Earlier work this paper cites.
Creusot: A Foundry for the Deductive Verification of Rust Programs. In Formal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Madrid, Spain, October 24-27, 2022, Proceedings (Lecture Notes in Computer Science, Vol. 13478) . Springer, 90–105
Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. 2022 · 2022
Earlier work this paper cites.
Diversity-Driven Automated Formal Verification. In 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022 . ACM, 1–13
Emily First and Yuriy Brun. 2022 · 2022
Earlier work this paper cites.
Aeneas: Rust verification by functional translation
Son Ho and Jonathan Protzenko. 2022 · 2022
Cited alongside, same era.
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022
Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, and Mateja Jamnik. 2022 · 2022
Cited alongside, same era.
RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. In PLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022 . ACM, 841–856
Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, and Derek Dreyer. 2022 · 2022
Cited alongside, same era.
Atmosphere: Towards Practical Verified Kernels in Rust. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification, KISV 2023, Koblenz, Germany, 23 October 2023 . ACM, 9–17
Xiangdong Chen, Zhaofeng Li, Lukas Mesicek, Vikram Narayanan, and Anton Burtsev. 2023 · 2023
Storage systems with verified correctness properties
Microsoft. 2024 · 2024
Closest in time.
Towards AI-Assisted Synthesis of Verified Dafny Methods
Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. 2024 · 2024
Closest in time.
Laurel: Generating Dafny Assertions Using Large Language Models
Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, and Yuanyuan Zhou. 2024 · 2024
Closest in time.
BACK TO THE BUILDING BLOCKS: A PATH TOWARD SECURE AND MEASURABLE SOFTWARE
Office of the National Cyber Director. 2024 · 2024
Closest in time.
How Rust went from a side project to the world’s most-loved programming language
MIT Technology Review. 2023 · 2024
Closest in time.
"Rust continues to be the most-admired programming language"
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Large Language Models Are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Models. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, Seattle, WA, USA, July 17-21, 2023 . ACM, 423–435
Yinlin Deng, Chunqiu Steven Xia, Haoran Peng, Chenyuan Yang, and Lingming Zhang. 2023 · 2023
Cited alongside, same era.
Baldur: Whole-Proof Generation and Repair with Large Language Models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2023, San Francisco, CA, USA, December 3-9, 2023 . ACM, 1229–1241
Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023 · 2023
Cited alongside, same era.
Finding Inductive Loop Invariants using Large Language Models
Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma. 2023 · 2023
Cited alongside, same era.
Verus: Verifying Rust Programs using Linear Ghost Types
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023 · 2023
Cited alongside, same era.
Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation. In Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023
Jiawei Liu, Chunqiu Steven Xia, Yuyao Wang, and Lingming Zhang. 2023 · 2023
Cited alongside, same era.
Keep the Conversation Going: Fixing 162 out of 337 bugs for $0.42 each using ChatGPT
Chunqiu Steven Xia and Lingming Zhang. 2023 · 2023
Cited alongside, same era.
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. 2023 · 2023
Cited alongside, same era.
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu K. Lahiri, and Nikhil Swamy. 2024 · 2024
Cited alongside, same era.
Stackoverflow. 2024b · 2024
Closest in time.
Clover: Closed-Loop Verifiable Code Generation. In AI Verification - First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22-23, 2024, Proceedings (Lecture Notes in Computer Science, Vol. 14846) . Springer, 134–155
Chuyue Sun, Ying Sheng, Oded Padon, and Clark W. Barrett. 2024b · 2024
Closest in time.
Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024 . USENIX Association, 649–666
Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. 2024a · 2024
Closest in time.
How Open Source Projects are Using Kani to Write Better Software in Rust | AWS Open Source Blog
The Kani Team. 2024 · 2024
Closest in time.
DebugBench: Evaluating Debugging Capability of Large Language Models
Runchu Tian, Yining Ye, Yujia Qin, Xin Cong, Yankai Lin, Yinxu Pan, Yesai Wu, Haotian Hui, Weichuan Liu, Zhiyuan Liu, and Maosong Sun. 2024 · 2024
Closest in time.
LEGO-Prover: Neural Theorem Proving with Growing Libraries. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024 . OpenReview.net
Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. 2024 · 2024
Closest in time.
Lemur: Integrating Large Language Models in Automated Program Verification. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024 . OpenReview.net
Haoze Wu, Clark W. Barrett, and Nina Narodytska. 2024 · 2024
Closest in time.
Whitefox: White-box compiler fuzzing empowered by large language models
Chenyuan Yang, Yinlin Deng, Runyu Lu, Jiayi Yao, Jiawei Liu, Reyhaneh Jabbarvand, and Lingming Zhang. 2024 · 2024
Closest in time.
VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024 . USENIX Association, 599–614
Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, and Weidong Cui. 2024 · 2024
Closest in time.
What’s in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
Rijul Jain, Shraddha Barke, Gabriel Ebner, Md Rakib Hossain Misu, Shan Lu, and Sarah Fakhoury. 2025 · 2025
Closest in time.
PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection
Hayley LeBlanc, Jacob R Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, and Vijay Chidambaram. 2025 · 2025
Closest in time.
"2024 Developer Survey: AI tools at development process; Challenges with AI at work"
Stackoverflow. 2024a · 2025
Closest in time.
Kernelgpt: Enhanced kernel fuzzing via large language models. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2 . 560–573
Chenyuan Yang, Zijie Zhao, and Lingming Zhang. 2025 · 2025
Closest in time.