AI Augmented ESBMC processing. Passes the output from ESBMC to an AI model that allows the user to use natural language to understand the output. As the output from ESBMC can be quite technical in nature. The AI can also be asked other questions, such as suggestions on how to fix the problem outputted by ESBMC, and to offer further explanations.
This is an area of research. From the ESBMC GitHub:
The efficient SMT-based context-bounded model checker (ESBMC)
demo.webm
- ESBMC-AI does not come with the original ESBMC software. In order to use ESBMC-AI you must provide ESBMC. Download ESBMC executable or build from source.
- Create a .env file using the provided .env.example as a template, and, insert your OpenAI API key.
- Enter the ESBMC executable location in the .env
ESBMC_PATH. - Further adjust .env settings as required.
- You can now run ESBMC-AI.
The following settings are adjustable in the .env file, this list may be incomplete:
OPENAI_API_KEY: This is required. Your OpenAI API key.CHAT_TEMPERATURE: The temperature parameter used when calling the chat completion API.AI_MODEL: The model to use. Options:gpt-3.5-turbo,gpt-4(under API key conditions).ESBMC_PATH: Override the default ESBMC path. Leave blank to use the default ("./esbmc").
./main.py /path/to/source_code.c./main.py -h/help
Pull requests are welcome. For major changes, please open an issue first to discuss what you would like to change.
Please make sure to update tests as appropriate.