This repo contains the source code for the paper Lemur: Integrating Large Language Models in Automated Program Verification

The implementation is tested on python3.8.10, but should work on more recent python versions.

The Python package dependencies can be installed by

pip install -r requirements.txt

You also need a working OPEN API key, and set the environment variable OPENAI_API_KEY.

export OPENAI_API_KEY=YOUR_KEY

You need to download two software verification tools by running

./build.sh

Important: UAutomizer depends on Java (sudo apt install openjdk-11-jdk)

To test UAutomizer, run:

python3 -u ./tools/uautomizer/Ultimate.py --spec ./lemur/benchmarks/sv_comp/properties/unreach-call.prp --file ./code2inv/benchmarks/code2inv/c/3.c --architecture 32bit --full-output

The program should finish in a few seconds and the last few lines should be

Execution finished normally
Writing output log to file Ultimate.log
Result:
TRUE

There are two experiments that we performed. The source code as well as the log files for each are contained in "code2inv/" and "lemur/", respectively.

@inproceedings{wu2023lemur,
  title={Lemur: Integrating Large Language Models in Automated Program Verification},
  author={Wu, Haoze and Barrett, Clark and Narodytska, Nina},
  booktitle={The Twelfth International Conference on Learning Representations},
  year={2024}
}