KeY Symposium 2025

General

The KeY system is a formal software development tool integrating design, implementation, formal specification, and formal verification of object-oriented software. At the core of the system is a theorem prover for the first-order Dynamic Logic of the respective target language, in particular Java, with a user-friendly graphical interface.

The KeY Symposium brings together researchers interested in KeY and related aspects. We will exchange recent achievements, current ideas, discuss the next steps and milestones of the area, as well as future directions in general. Also the latest developments in the KeY tool are presented and discussed.

Important Dates

Deadline for registration: 19th May [Registration Form]

Symposium: 5th – 8th August

Venue

The KeY Symposium takes place at Chalet Giersch located in the French alps.

Address
Chalet l’Eridan
84 Chemin du Plan du Mont
F – 74230 MANIGOD

Maps: OpenStreetMap, Google Maps, Apple Maps,

How to participate?

Please, register until Monday, May 19th using the registration form, if you plan to attend the KeY Symposium.

How to contribute?

We plan with two types of talks for the symposium:i

  • a standard talk with ca. 25 to 30 min incl. discussion, and
  • a short talk 15 min incl. discussions

Depending on time and interest: breakout sessions, panel discussion. More details come later.

Schedule

Arrival day is the 5th August. In the evening we will have a welcome dinner at the Chalet. The scientific programme starts Wednesday, 6th August at 9 a.m.

The technical programme will be published End of June / Begin July


Organisation Committee


Previous KeY-Workshop

A list of all recent KeY workshops is available here.