Skip to content

2nd Hackeython

Jump to bottom
Wolfram Pfeifer edited this page Feb 16, 2024 · 39 revisions

Days

21/22. Februrary 2024

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

Venue

Karlsruhe

Topics

Larger Group Topics

  • 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

  • Visions on how the project management workflow is to look in the future. Shepard: Daniel

    • Verification Template -- Providing the best suitable environment for making the side-task of Java verification an ease.

  • Remote Procedure API -- Infrastructure on KeY side ready, need a client in Python or other language Shepard: Alexander

  • 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

  • Idea: Verification from the perspective of an algorithm verification engineer.

  • Idea: Destructors (observers) for user-defined ADTS. Shepard: Mattias (?) (Alexander who implemented ADTs (?))

  • Idea: SMT translation without type embedding/hierarchy (u2i, i2u functions etc.) Shepard: Wolfram (?)

  • Idea: Organizing sorts/functions/predicates and taclets in "theories" Shepard: Wolfram (?): The idea would be that instead of the current taclet base where (nearly) all taclets are loaded by default, the standard .key files are organized in a hierarchy (via includes). If now for example the user loads the aunt agatha example, the .key file would contain something like \include "FOL"; (which again would include PROP). Another benefit would be that this would provide clear namespaces for symbols. Caveat: I am not sure if this topic is simple enough for the HacKeYthon. We would also probably need knowledge from Alexander about the KeYParser and name resolution.

Issues/PRs

Issues

  • Support for JML TYPE #3407
  • Missing rule for type of array #3389
  • AutoModeAction cannot be started when proof tree or task tree is selected #3208
  • add nice-to-write syntactic sugar for sequence construction #395
  • Non-trivial diverges clauses make you prove things twice. #29

PRs

  • Revive work on Polymorphic Sorts #3384
  • Introduce relevant JML aliases ('assigns', 'loop_modifies' and 'loop_writes') #3365
  • Create a JSON-RPC for KeY #3303

Social Event

  • Wednesday at 7pm: Dinner at Vogelbräu
Clone this wiki locally