Leveraging Large Language Models for Automated Proof Synthesis in Rust

Dafny: An automatic program verifier for functional correctness

K Rustan M Leino · 2010

Earlier work this paper cites.

Learning universally quantified invariants of linear data structures

Pranav Garg, Christof Löding, P Madhusudan, and Daniel Neider · 2013

Earlier work this paper cites.

IronFleet: Proving practical distributed systems correct

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Michael L Roberts, Srinath Setty, and Brian Zill · 2015

Earlier work this paper cites.

Learning invariants using decision trees and implication counterexamples

Pranav Garg, Daniel Neider, P. Madhusudan, and Dan Roth · 2016

Earlier work this paper cites.

Data-driven precondition inference with learned features

Saswat Padhi, Rahul Sharma, and Todd Millstein · 2016

Earlier work this paper cites.

Hammer for coq: Automation for dependent type theory

Łukasz Czajka and Cezary Kaliszyk · 2018

Earlier work this paper cites.

Learning loop invariants for program verification

Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song · 2018

Earlier work this paper cites.

Quantified invariants via syntax-guided synthesis

Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta · 2019

Earlier work this paper cites.

I4: Incremental inference of inductive invariants for verification of distributed protocols

Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A Sakallah · 2019

Cited alongside, same era.

Learning to prove theorems via interacting with proof assistants

Kaiyu Yang and Jia Deng · 2019

Cited alongside, same era.

Practical proof search for coq by type inhabitation

Łukasz Czajka · 2020

Cited alongside, same era.

Storage Systems are Distributed Systems (So Verify Them That Way!)

Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno · 2020

Cited alongside, same era.

Data-driven inference of representation invariants

Anders Miltner, Saswat Padhi, Todd Millstein, and David Walker · 2020

Cited alongside, same era.

Cln2inv: Learning loop invariants with continuous logic networks

Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana · 2020

Beyond the elementary representations of program invariants over algebraic data types

Yurii Kostyukov, Dmitry Mordvinov, and Grigory Fedyukovich · 2021

Later among the works it cites.

Inferring invariants with quantifier alternations: Taming the search space explosion

Jason R. Koenig, Oded Padon, Sharon Shoham, and Alex Aiken · 2022

Later among the works it cites.

Induction duality: Primal-dual search for invariants

Oded Padon, James R Wilcox, Jason R Koenig, Kenneth L McMillan, and Alex Aiken · 2022

Later among the works it cites.

DuoAI: Fast, automated inference of inductive invariants for verifying distributed protocols

Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh · 2022

Later among the works it cites.

Baldur: whole-proof generation and repair with large language models

Original

Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun · 2023

Closest in time.