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”
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”
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.
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”