Finding Inductive Loop Invariants using Large Language Models

An axiomatic basis for computer programming

Hoare, C. A. R · 1969

Earlier work this paper cites.

Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints

Cousot, P., and Cousot, R · 1977

Earlier work this paper cites.

Automatic predicate abstraction of C programs

Ball, T., Majumdar, R., Millstein, T. D., and Rajamani, S. K · 2001

Earlier work this paper cites.

Houdini, an annotation assistant for esc/java

Flanagan, C., and Leino, K. R. M · 2001

Earlier work this paper cites.

A static analyzer for large safety-critical software

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X · 2003

Earlier work this paper cites.

Counterexample-guided abstraction refinement for symbolic model checking

Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., and Veith, H · 2003

Earlier work this paper cites.

Interpolation and sat-based model checking

McMillan, K. L · 2003

Earlier work this paper cites.

Boogie: A modular reusable verifier for object-oriented programs

Barnett, M., Chang, B. E., DeLine, R., Jacobs, B., and Leino, K. R. M · 2005

Earlier work this paper cites.

Z3: An efficient smt solver

de Moura, L., and Bjørner, N · 2008

Earlier work this paper cites.

Syntax-guided synthesis

Alur, R., Bodik, R., Juniwal, G., Martin, M. M., Raghothaman, M., Seshia, S. A., Singh, R., Solar-Lezama, A., Torlak, E., and Udupa, A · 2013

Earlier work this paper cites.

Frama-c: A software analysis perspective

Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., and Yakobowski, B · 2015

Earlier work this paper cites.

Accelerating invariant generation

Madhukar, K., Wachter, B., Kroening, D., Lewis, M., and Srivas, M · 2015

Cited alongside, same era.

The Satisfiability Modulo Theories Library (SMT-LIB)

Barrett, C., Fontaine, P., and Tinelli, C · 2016

Cited alongside, same era.

Learning invariants using decision trees and implication counterexamples

Garg, P., Neider, D., Madhusudan, P., and Roth, D · 2016

Cited alongside, same era.

Data-driven precondition inference with learned features

Padhi, S., Sharma, R., and Millstein, T. D · 2016

Cited alongside, same era.

Learning shape analysis

Brockschmidt, M., Chen, Y., Kohli, P., Krishna, S., and Tarlow, D · 2017

Cited alongside, same era.

Alt-Ergo 2.2

Conchon, S., Coquereau, A., Iguernlala, M., and Mebsout, A · 2018

Cited alongside, same era.

Learning nonlinear loop invariants with gated continuous logic networks

Yao, J., Ryan, G., Wong, J., Jana, S., and Gu, R · 2020

Later among the works it cites.

Evaluating large language models trained on code, 2021

Chen, M., Tworek, J., Jun, H., Yuan, Q., de Oliveira Pinto, H. P., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., Ray, A., Puri, R., Krueger, G., Petrov, M., Khlaaf, H., Sastry, G., Mishkin, P., Chan, B., Gray, S., Ryder, N., Pavlov, M., Power, A., Kaiser, L., Bavarian, M., Winter, C., Tillet, P., Such, F. P., Cummings, D., Plappert, M., Chantzis, F., Barnes, E., Herbert-Voss, A., Guss, W. H., Nichol, A., Paino, A., Tezak, N., Tang, J., Babuschkin, I., Balaji, S., Jain, S., Saunders, W., Hesse, C., Carr, A. N., Leike, J., Achiam, J., Misra, V., Morikawa, E., Radford, A., Knight, M., Brundage, M., Murati, M., Mayer, K., Welinder, P., McGrew, B., Amodei, D., McCandlish, S., Sutskever, I., and Zaremba, W · 2021

Later among the works it cites.

Github copilot

GitHub · 2022

Later among the works it cites.

Amazon codewhisperer

Amazon · 2023

Closest in time.

Competition on software verification and witness validation: Sv-comp 2023

Beyer, D · 2023

Closest in time.