Next Steps in LLM-Supported Java Verification
We evaluate the effectiveness of feedback provided to a Large Language Model by the theorem prover KeY for verification of Java software using LLM-generated auxilliary annotations.
15. Dec 2024
Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification
We evaluate the potential of Large Language Models (specifically GPT 3.5 and GPT 4o) for the generation of code annotations in the Java Modelling Language using a prototypical integration of the Java verification tools KeY and JJBMC with OpenAI's API.
27. Oct 2024