Fetching the paper…
Reading the bibliography…
Large language models show great promise in many domains, including programming.
Prompting Is Programming: A Query Language for Large Language Models
Luca Beurer-Kellner, Marc Fischer, and Martin T. Vechev. 2023 · 1969
Earlier work this paper cites.
An Axiomatic Basis for Computer Programming
C. A. R. Hoare. 1969 · 1969
Earlier work this paper cites.
Applying ’Design by Contract’
Bertrand Meyer. 1992 · 1992
Earlier work this paper cites.
Selected Papers on Automath
R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer (Eds.). 1994 · 1994
Earlier work this paper cites.
An extended static checker for Modula-3. In International Conference on Compiler Construction . Springer, 302–305
K. Rustan M. Leino and Greg Nelson. 1998 · 1998
Earlier work this paper cites.
Understanding interobserver agreement: the kappa statistic
Anthony J Viera, Joanne M Garrett, et al · 2005
Earlier work this paper cites.
Z3: An Efficient SMT Solver. In TACAS . 337–340
Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008 · 2008
Earlier work this paper cites.
seL4: formal verification of an OS kernel.. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009 , Jeanna Neefe Matthews and Thomas E. Anderson (Eds.). ACM, 207–220
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009 · 2009
Earlier work this paper cites.
Formal verification of a realistic compiler
Xavier Leroy. 2009 · 2009
Earlier work this paper cites.
Validity Threats in Empirical Software Engineering Research - An Initial Survey. In Proceedings of the 22nd International Conference on Software Engineering & Knowledge Engineering (SEKE’2010), Redwood City, San Francisco Bay, CA, USA, July 1 - July 3, 2010 . Knowledge Systems Institute Graduate School, 374–379
Robert Feldt and Ana Magazinius. 2010 · 2010
Earlier work this paper cites.
Towards Formally Verified Optimizing Compilation in Flight Control Software. In Bringing Theory to Practice: Predictability and Performance in Embedded Systems, DATE Workshop PPES 2011, March 18, 2011, Grenoble, France (OASIcs, Vol. 18) , Philipp Lucas, Lothar Thiele, Benoit Triquet, Theo Ungerer, and Reinhard Wilhelm (Eds.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 59–68
Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. 2011 · 2011
Earlier work this paper cites.
The Boogie Verification Debugger (Tool Paper)
Claire Le Goues, K. Rustan M. Leino, and Michal Moskal. 2011 · 2011
Earlier work this paper cites.
Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011 , Mary W. Hall and David A. Padua (Eds.). ACM, 283–294
Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011 · 2011
Earlier work this paper cites.
Computing inter-rater reliability for observational data: an overview and tutorial
Kevin A Hallgren. 2012 · 2012
Earlier work this paper cites.
seL4: From General Purpose to a Proof of Information Flow Enforcement. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013 . IEEE Computer Society, 415–429
Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. 2013 · 2013
Earlier work this paper cites.
Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI ’14, Broomfield, CO, USA, October 6-8, 2014 , Jason Flinn and Hank Levy (Eds.). USENIX Association, 165–181
Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014 · 2014
Earlier work this paper cites.
IronFleet: proving practical distributed systems correct. In SOSP , Ethan L. Miller and Steven Hand (Eds.). ACM, 1–17
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. 2015 · 2015
Earlier work this paper cites.
Views on Internal and External Validity in Empirical Software Engineering. In 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Volume 1 , Antonia Bertolino, Gerardo Canfora, and Sebastian G. Elbaum (Eds.). IEEE Computer Society, 9–19
Janet Siegmund, Norbert Siegmund, and Sven Apel. 2015 · 2015
Earlier work this paper cites.
Program Synthesis
Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. 2017 · 2017
Earlier work this paper cites.
Accessible Software Verification with Dafny
K. Rustan M. Leino. 2017 · 2017
Earlier work this paper cites.
A Survey of Machine Learning for Big Code and Naturalness
Miltiadis Allamanis, Earl T. Barr, Premkumar T. Devanbu, and Charles Sutton. 2018 · 2018
Earlier work this paper cites.
Formal Reasoning About the Security of Amazon Web Services. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 10981) , Hana Chockler and Georg Weissenbacher (Eds.). Springer, 38–47
Byron Cook. 2018 · 2018
Earlier work this paper cites.
Hammer for Coq: Automation for Dependent Type Theory
Lukasz Czajka and Cezary Kaliszyk. 2018 · 2018
Earlier work this paper cites.
Improving language understanding by generative pre-training
Alec Radford, Karthik Narasimhan, Tim Salimans, Ilya Sutskever, et al · 2018
Earlier work this paper cites.
Temporal Logic
Hillel Wayne. 2018 · 2018
Earlier work this paper cites.
SPoC: Search-based Pseudocode to Code. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada , Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garnett (Eds.). 11883–11894
Sumith Kulal, Panupong Pasupat, Kartik Chandra, Mina Lee, Oded Padon, Alex Aiken, and Percy Liang. 2019 · 2019
Earlier work this paper cites.
QED at Large: A Survey of Engineering of Formally Verified Software
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. 2019 · 2019
Earlier work this paper cites.
An Empirical Study on Learning Bug-Fixing Patches in the Wild via Neural Machine Translation
Michele Tufano, Cody Watson, Gabriele Bavota, Massimiliano Di Penta, Martin White, and Denys Poshyvanyk. 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) , Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.). PMLR, 6984–6994
Kaiyu Yang and Jia Deng. 2019 · 2019
Earlier work this paper cites.
Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2020 · 2020
Earlier work this paper cites.
TacTok: semantics-aware proof synthesis
Emily First, Yuriy Brun, and Arjun Guha. 2020 · 2020
Earlier work this paper cites.
The 2020 expert survey on formal methods. In International Conference on Formal Methods for Industrial Critical Systems . Springer, 3–69
Hubert Garavel, Maurice H Ter Beek, and Jaco Van De Pol. 2020 · 2020
Earlier work this paper cites.
Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks. In Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual , Hugo Larochelle, Marc’Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin (Eds.)
Patrick S. H. Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen-tau Yih, Tim Rocktäschel, Sebastian Riedel, and Douwe Kiela. 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 , Koushik Sen and Mayur Naik (Eds.). ACM, 1–10
Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner. 2020 · 2020
Earlier work this paper cites.
Graph-based, Self-Supervised Program Repair from Diagnostic Feedback. In Proceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtual Event (Proceedings of Machine Learning Research, Vol. 119) . PMLR, 10799–10808
Michihiro Yasunaga and Percy Liang. 2020 · 2020
Cited alongside, same era.
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
Cited alongside, same era.
Satisfiability Modulo Theories
Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2021 · 2021
Cited alongside, same era.
On Multi-Modal Learning of Editing Source Code. In 36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021, Melbourne, Australia, November 15-19, 2021 . IEEE, 443–455
Saikat Chakraborty and Baishakhi Ray. 2021 · 2021
Cited alongside, same era.
Automated reasoning
Amazon. 2023 · 2023
Later among the works it cites.
The Internal State of an LLM Knows When It’s Lying. In Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023 , Houda Bouamor, Juan Pino, and Kalika Bali (Eds.). Association for Computational Linguistics, 967–976
Amos Azaria and Tom M. Mitchell. 2023 · 2023
Later among the works it cites.
Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings (Lecture Notes in Computer Science, Vol. 14000) , Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker (Eds.). Springer, 571–583
Franck Cassez, Joanne Fuller, Milad K. Ghale, David J. Pearce, and Horacio Mijail Anton Quiles. 2023 · 2023
Later among the works it cites.
Boosting Transformers and Language Models for Clinical Prediction in Immunotherapy. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 5: Industry Track) , Sunayana Sitaram, Beata Beigman Klebanov, and Jason D Williams (Eds.). Association for Computational Linguistics, Toronto, Canada, 332–340
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
The Internet of Things
Samuel Greengard. 2021 · 2021
Cited alongside, same era.
Theories of Programming: The Life and Works of Tony Hoare
Cliff B Jones and Jayadev Misra. 2021 · 2021
Cited alongside, same era.
Evaluating Large Language Models Trained on Code
Mark Chen et al. 2021 · 2021
Cited alongside, same era.
Applying CodeBERT for Automated Program Repair of Java Simple Bugs. In MSR . 505–509
Ehsan Mashhadi and Hadi Hemmati. 2021 · 2021
Cited alongside, same era.
Prompt Programming for Large Language Models: Beyond the Few-Shot Paradigm. In CHI ’21: CHI Conference on Human Factors in Computing Systems, Virtual Event / Yokohama Japan, May 8-13, 2021, Extended Abstracts , Yoshifumi Kitamura, Aaron Quigley, Katherine Isbister, and Takeo Igarashi (Eds.). ACM, 314:1–314:7
Laria Reynolds and Kyle McDonell. 2021 · 2021
Cited alongside, same era.
CodeT5: Identifier-aware Unified Pre-trained Encoder-Decoder Models for Code Understanding and Generation. In EMNLP
Y. Wang, W. Wang, S.R. Joty, and S.C.H. Hoi. 2021 · 2021
Cited alongside, same era.
PaLM: Scaling Language Modeling with Pathways
Aakanksha Chowdhery et al. 2022 · 2022
Cited alongside, same era.
PromptSource: An Integrated Development Environment and Repository for Natural Language Prompts. In Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics, ACL 2022 - System Demonstrations, Dublin, Ireland, May 22-27, 2022 , Valerio Basile, Zornitsa Kozareva, and Sanja Stajner (Eds.). Association for Computational Linguistics, 93–104
Stephen H. Bach, Victor Sanh, Zheng Xin Yong, Albert Webson, Colin Raffel, Nihal V. Nayak, Abheesht Sharma, Taewoon Kim, M. Saiful Bari, Thibault Févry, Zaid Alyafeai, Manan Dey, Andrea Santilli, Zhiqing Sun, Srulik Ben-David, Canwen Xu, Gunjan Chhablani, Han Wang, Jason Alan Fries, Maged Saeed AlShaibani, Shanya Sharma, Urmish Thakker, Khalid Almubarak, Xiangru Tang, Dragomir R. Radev, Mike Tian-Jian Jiang, and Alexander M. Rush. 2022 · 2022
Cited alongside, same era.
Zekai Chen, Mariann Micsinai Balan, and Kevin Brown. 2023 · 2023
Later among the works it cites.
Amazon CodeWhisperer
Amazon CodeWhisperer. 2023 · 2023
Later among the works it cites.
CompCert
CompCert. 2023 · 2023
Later among the works it cites.
GitHub Copilot
GitHub Copilot. 2023 · 2023
Later among the works it cites.
dafny-lang
Dafny. 2023 · 2023
Later among the works it cites.
The Infinite Index: Information Retrieval on Generative Text-To-Image Models. In Proceedings of the 2023 Conference on Human Information Interaction and Retrieval, CHIIR 2023, Austin, TX, USA, March 19-23, 2023 , Jacek Gwizdka and Soo Young Rieh (Eds.). ACM, 172–186
Niklas Deckers, Maik Fröbe, Johannes Kiesel, Gianluca Pandolfo, Christopher Schröder, Benno Stein, and Martin Potthast. 2023 · 2023
Later among the works it cites.
Case Studies of Development of Verified Programs with Dafny for Accessibility Assessment. In Fundamentals of Software Engineering - 10th International Conference, FSEN 2023, Tehran, Iran, May 4-5, 2023, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 14155) , Hossein Hojjat and Erika Ábrahám (Eds.). Springer, 25–39
João Pascoal Faria and Rui Abreu. 2023 · 2023
Later among the works it cites.
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 , Satish Chandra, Kelly Blincoe, and Paolo Tonella (Eds.). ACM, 1229–1241
Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023 · 2023
Later among the works it cites.
Mathematical Capabilities of ChatGPT
Simon Frieder, Luca Pinchetti, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Christian Petersen, Alexis Chevalier, and Julius Berner. 2023 · 2023
Later among the works it cites.
Truth-O-Meter: Collaborating with LLM in Fighting its Hallucinations
Boris A. Galitsky. 2023 · 2023
Later among the works it cites.
GCC, the GNU Compiler Collection
GCC. 2023 · 2023
Later among the works it cites.
Performance Improvements via Formally-Verified Cryptography in Firefox
Kevin Jacobs and Benjamin Beurdouche. 2022 · 2023
Later among the works it cites.
Program Proofs
K. Rustan M. Leino. 2023 · 2023
Later among the works it cites.
Making Language Models Better Reasoners with Step-Aware Verifier. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) , Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki (Eds.). Association for Computational Linguistics, Toronto, Canada, 5315–5333
Yifei Li, Zeqi Lin, Shizhuo Zhang, Qiang Fu, Bei Chen, Jian-Guang Lou, and Weizhu Chen. 2023 · 2023
Later among the works it cites.
The LLVM Compiler Infrastructure
LLVM. 2023 · 2023
Later among the works it cites.
Sources of Hallucination by Large Language Models on Inference Tasks. In Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023 , Houda Bouamor, Juan Pino, and Kalika Bali (Eds.). Association for Computational Linguistics, 2758–2774
Nick McKenna, Tianyi Li, Liang Cheng, Mohammad Javad Hosseini, Mark Johnson, and Mark Steedman. 2023 · 2023
Later among the works it cites.
The Dafny Programming and Verification Language
Microsoft. 2023a · 2023
Later among the works it cites.
Microsoft Research
Microsoft. 2023b · 2023
Later among the works it cites.
Retrieval-Based Prompt Selection for Code-Related Few-Shot Learning. In 45th IEEE/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, May 14-20, 2023 . IEEE, 2450–2462
Noor Nashid, Mifta Sintaha, and Ali Mesbah. 2023 · 2023
Later among the works it cites.
OpenAI. 2023a · 2023
Later among the works it cites.
Reasoning with Language Model Prompting: A Survey. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023 , Anna Rogers, Jordan L. Boyd-Graber, and Naoaki Okazaki (Eds.). Association for Computational Linguistics, 5368–5393
Shuofei Qiao, Yixin Ou, Ningyu Zhang, Xiang Chen, Yunzhi Yao, Shumin Deng, Chuanqi Tan, Fei Huang, and Huajun Chen. 2023 · 2023
Later among the works it cites.
Rohan Anil et al. 2023 · 2023
Later among the works it cites.
Code llama: Open foundation models for code
Baptiste Rozière, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Tal Remez, Jérémy Rapin, et al · 2023
Later among the works it cites.
Artificial intelligence hallucinations
M. Salvagno and A.G. Taccone, F.S.and Gerli. 2023 · 2023
Later among the works it cites.
Passport: Improving Automated Formal Verification Using Identifiers
Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. 2023 · 2023
Later among the works it cites.
The seL4® Microkernel
seL4 Project. 2023 · 2023
Later among the works it cites.
Katana: Dual Slicing Based Context for Learning Bug Fixes
Mifta Sintaha, Noor Nashid, and Ali Mesbah. 2023 · 2023
Later among the works it cites.
Automating Code-Related Tasks Through Transformers: The Impact of Pre-training. In 45th IEEE/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, May 14-20, 2023 . IEEE, 2425–2437
Rosalia Tufano, Luca Pascarella, and Gabriele Bavota. 2023 · 2023
Later among the works it cites.
CodeT5+: Open Code Large Language Models for Code Understanding and Generation
Yue Wang, Hung Le, Akhilesh Gotmare, Nghi D. Q. Bui, Junnan Li, and Steven C. H. Hoi. 2023 · 2023
Later among the works it cites.
Towards A Correct-by-Construction FHE Model
Zhenkun Yang, Wen Wang, Jeremy Casas, Pasquale Cocchini, and Jin Yang. 2023 · 2023
Later among the works it cites.
Learn ’em Dafny. In Dafny Workshop at POPL (London, England)
James Noble. 2024 · 2024
Closest in time.