This is a placeholder issue for a topic of the 3rd HacKeYthon, where the idea is to create a small demonstrator (probably in Python) which implements a ping-pong game between and KeY and LLMs for specification inference/generation. The goal is to extract certain information from KeY, for example information about the open branches after a verification attempt, via the REST-API.
The work will build on #3303.
This is a placeholder issue for a topic of the 3rd HacKeYthon, where the idea is to create a small demonstrator (probably in Python) which implements a ping-pong game between and KeY and LLMs for specification inference/generation. The goal is to extract certain information from KeY, for example information about the open branches after a verification attempt, via the REST-API.
The work will build on #3303.