Laurel: Unblocking Automated Verification with Large Language Models

Learning to Prove Theorems via Interacting with Proof Assistants

Original

Kaiyu Yang and Jia Deng. 2019 · 1905

Earlier work this paper cites.

Assigning meanings to programs

R.W. Floyd. 1967 · 1967

Earlier work this paper cites.

The String-to-String Correction Problem

Robert A. Wagner and Michael J. Fischer. 1974 · 1974

Earlier work this paper cites.

Simple Fast Algorithms for the Editing Distance between Trees and Related Problems

Kaizhong Zhang and Dennis Shasha. 1989 · 1989

Earlier work this paper cites.

JPlag: Finding plagiarisms among a set of programs

Lutz Prechelt and Michael Phlippsen. 2000 · 2000

Earlier work this paper cites.

Generating error traces from verification-condition counterexamples

K. Rustan M. Leino, Todd Millstein, and James B. Saxe. 2005 · 2005

Earlier work this paper cites.

DECKARD: Scalable and Accurate Tree-Based Detection of Code Clones. In 29th International Conference on Software Engineering (ICSE’07) . 96–105

Lingxiao Jiang, Ghassan Misherghi, Zhendong Su, and Stephane Glondu. 2007 · 2007

Earlier work this paper cites.

Z3: An Efficient SMT Solver. In TACAS

Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008 · 2008

Earlier work this paper cites.

This is Boogie 2

K. Rustan M. Leino. 2008 · 2008

Earlier work this paper cites.

NICAD: Accurate Detection of Near-Miss Intentional Clones Using Flexible Pretty-Printing and Code Normalization. In 2008 16th IEEE International Conference on Program Comprehension . 172–181

Chanchal K. Roy and James R. Cordy. 2008 · 2008

Earlier work this paper cites.

Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning , Edmund M. Clarke and Andrei Voronkov (Eds.)

K. Rustan M. Leino. 2010 · 2010

Earlier work this paper cites.

Why3 — Where Programs Meet Provers. In Programming Languages and Systems , Matthias Felleisen and Philippa Gardner (Eds.)

Jean-Christophe Filliâtre and Andrei Paskevich. 2013 · 2013

Earlier work this paper cites.

Software Model Checking for People Who Love Automata. In CAV , Natasha Sharygina and Helmut Veith (Eds.)

Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2013 · 2013

Earlier work this paper cites.

Semantic code clone detection using parse trees and grammar recovery. In Confluence 2013: The Next Generation Information Technology Summit (4th International Conference) . 41–46

Rajkumar Tekchandani, Rajesh Kumar Bhatia, and Maninder Singh. 2013 · 2013

Earlier work this paper cites.

A Source Code Similarity System for Plagiarism Detection

Zoran Đurić and Dragan Gašević. 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) . USENIX Association, Broomfield, CO, 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.

LiquidHaskell: experience with refinement types in the real world. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell

Niki Vazou, Eric L. Seidel, and Ranjit Jhala. 2014 · 2014

Earlier work this paper cites.

Detecting Android Malware Using Clone Detection

Jian Chen, Manar H. Alalfi, Thomas R. Dean, and Ying Zou. 2015 · 2015

Earlier work this paper cites.

Deductive Software Verification - The KeY Book - From Theory to Practice

Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich (Eds.). 2016 · 2016

Earlier work this paper cites.

Dependent Types and Multi-Monadic Effects in F*. In Principles of Programming Languages (POPL)

Nikhil Swamy, Cătălin Hriţcu, 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.

Plagiarism detection in students’ programming assignments based on semantics: multimedia e-learning based smart assessment methodology

Farhan Ullah, Junfeng Wang, Muhammad Farhan, Sohail Jabbar, Zhiming Wu, and Shehzad Khalid. 2018 · 2018

Earlier work this paper cites.

code2vec: learning distributed representations of code

Uri Alon, Meital Zilberstein, Omer Levy, and Eran Yahav. 2019 · 2019

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.

Siamese: scalable and incremental code clone search via multiple code representations

Chaiyong Ragkhitwetsagul and Jens Krinke. 2019 · 2019

Earlier work this paper cites.

Everparse: verified secure zero-copy parsers for authenticated message formats. In Proceedings of the 28th USENIX Conference on Security Symposium (Santa Clara, CA, USA) (SEC’19) . USENIX Association, USA, 1465–1482

Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019 · 2019

Cited alongside, same era.

Design and Development of Software Tool for Code Clone Search, Detection, and Analysis. In 2019 3rd International conference on Electronics, Communication and Aerospace Technology (ICECA) . 1002–1006

Dethe Tukaram and Uma Maheswari B. 2019 · 2019

Cited alongside, same era.

Language models are few-shot learners (NIPS ’20)

Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. 2020 · 2020

Cited alongside, same era.

Flux: Liquid Types for Rust

Nico Lehmann, Adam T. Geller, Niki Vazou, and Ranjit Jhala. 2023 · 2023

Later among the works it cites.

Magnushammer: A Transformer-Based Approach to Premise Selection. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS’23

Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Bartosz Piotrowski, Albert Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. 2023 · 2023

Later among the works it cites.

Can Large Language Models Reason about Program Invariants?. In ICML 2023 , Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett (Eds.)

Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. [n. d.] · 2023

Later among the works it cites.

Selective Annotation Makes Language Models Better Few-Shot Learners. In The Eleventh International Conference on Learning Representations

Hongjin SU, Jungo Kasai, Chen Henry Wu, Weijia Shi, Tianlu Wang, Jiayi Xin, Rui Zhang, Mari Ostendorf, Luke Zettlemoyer, Noah A. Smith, and Tao Yu. 2023 · 2023

Later among the works it cites.