Posts
New Feature: State Merging in KeY
Current nightly builds of KeY contain a new feature called state merging, a technique to decrease the size of proof trees arising from the symbolic execution of large programs. Continue reading “New Feature: State Merging in KeY”
How researchers from UPM and IMDEA used KeY as backend
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. Continue reading “How researchers from UPM and IMDEA used KeY as backend”
The new KeY Book has been published
A years long effort comes to a successful conclusion. On December, 20th the new KeY book became available online. Most of the book’s content is new or largely rewritten compared to the first KeY Book.
KeY talk at the British Computer Society
Prof. Reiner Hähnle will give an invited talk at the British Computer Society at May 4th, 2017: “The KeY Formal Verification Tool“.
Continue reading “KeY talk at the British Computer Society”15th KeY Symposium 2016
Continue reading “15th KeY Symposium 2016”