2nd Hackeython

Days

21/22. Februrary 2024

both days: 10:00 am - 6:00 pm

Karlsruhe

JML-based Invariant Dialog -- Having an Invariant Dialog that follows the loop specification/clauses of JML and allows also to enter JML formula might provide an user-friendlier experience. No shephard needed.
Error Reporting Shepard: Matthias
Verification Template -- Providing the best suitable environment for making the side-task of Java verification an ease. Shepard: Alexander
Recoder Removal -- We should try to make progress on the removal of the Recoder framework in favor of the javaparser. Current state is debugging and fixing of pattern expression. Shepard: Alexander
Remote Procedure API -- Infrastructure on KeY side ready, need a client in Python or other language Shepard: Alexander
'System.out.println*' und häufig benötigte Systemfunktionen (wie ArraytoString) in JavaRedux deklarieren und u.U. teilweise auch spezifizieren Shepard: Wolfram
In the repo, there is a tag HacKeYthon. Please mark candidate issues and feature requests!
Idea: Look at how invariant/spec generation tools can be incorporated into the KeY workflow. ChatGPT, Daikon, ... That would be more playing around with what is there. Expected output: Recommendations on if/how such invariant candidate generators can be included into KeY easily. Shepard: Michael(?)
Idea: Visions on how the project management workflow is to look in the future.
Idea: Verification from the perspective of an algorithm verification engineer.