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
- Install required Python modules:
pip install -r requirements.txt. - 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. Some settings are allowed to be omitted, however, the program will display a warning when done so as it is not recommended. This list may be incomplete:
OPENAI_API_KEY: Your OpenAI API key.CHAT_TEMPERATURE: The temperature parameter used when calling the chat completion API. This controls the temperature sampling that the model uses. Higher values like 0.8 and above will make the output more random, on the other hand, lower values like 0.2 will be more deterministic. Allowed values are between 0.0 to 2.0. Default is 1.0.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").CFG_SYS_PATH: Path to JSON file that contains initial prompt messages for the AI model that give it instructions on how to function.CFG_INITIAL_PROMPT_PATH: Text file that contains the instructions to initiate the initial prompt, where the AI is asked to walk through the code and explain the ESBMC output.
./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.