Researchers (Julio Mariño Raúl, N. N. Alborodo, Lars-Åke Fredlund and Ángel Herranz) from UPM and IMDEA (both Madrid, Spain) developed a methodology to synthesize verifiable concurrent Java components from formal models. The implementation of their approach used the KeY verification system as backend.
Interested in their work and how the authors make use of KeY to verify properties for concurrent programs (which is not natively supported by KeY)? Head over to Springer and read their article “Synthesis of verifiable concurrent Java components from formal models”.
If you used or intend to use KeY as part of your own research, we would be interested to hear from you and for any feedback that can help to improve KeY.