2nd Hackeython

Organization

Information about the organization of the event (such as schedule and venue) can be found on the KeY website: https://www.key-project.org/2nd-hackeython-2024/

Some hints for the work in groups and KeY development in general are collected here: HacKeYthon-Hints

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 a user-friendlier experience. Shepard: Richard Topic page
Error Reporting Shepard: Mattias Topic page
Visions on how the project management workflow is to look in the future. Shepard: Daniel. Topic page
- Verification Template -- Providing the best suitable environment for making the side-task of Java verification an ease.
How to deal with missing library functions such as System.out.println* and other frequently used system functions (e.g. Arrays.toString())? Shepard: Wolfram Topic Page
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
Destructors (observers) for user-defined ADTS. Shepard: Mattias Topic page
SMT translation without type embedding/hierarchy (u2i, i2u functions etc.) Shepard: Wolfram Topic page

This page shows a list of bugs and existing (unfinished) PRs that might be good candidates for tasks to tackle during the HacKeYthon: