The KeY Formal Verification Tool (Jointly with Formal Methods Europe - FME)Date/Time: Thursday 4 May 2017, 5.15pm coffee/tea for 6.00pm start of talk.Venue: BCS, 1st Floor, The Davidson Building, 5 Southampton Street, London, WC2E 7HA | MapsSpeaker:Prof. Dr. Reiner Hähnle, TU Darmstadt, GermanyCost:FreeBook Online https://events.bcs.org/book/2357/ Only those who have booked a place via the BCS booking link will gain access to the building on the day.Synopsis:KeY is a deductive verification tool for sequential Java programs. It is based on a rich program logic for Java source code. KeY can perform functional verification of Java programs annotated with with specifications in the Java Modeling language. Specification elements include class invariants and method contracts. The rules of KeY's program logic realize a symbolic execution engine for Java. Verificationproceeds method-wise, unbounded loops are approximated by invariants, method calls by contracts. KeY incorporates state-of-art proof search and an auto-active mode that in many cases results in fully automatic proofs. Otherwise, the user can perform interactive steps or ask the system to search for a counter example. KeYhas been successfully used to verify complex legacy code, such as the JDK's sort method, where a subtle bug was found and subsequently fixed. I will explain some of the theoretical underpinnings and design principles of KeY. I will also give a live demonstration of some of KeY's capabilities.
Further information:
The KeY system can be downloaded and installed from http://www.key-project.org/download/releases/key26-pre/ webstart/KeY.jnlp
In December 2016, "Deductive Software Verification - The KeY Book" appeared as Springer LNCS volume 10001 - the definitive guide to KeY.Prof. Jonathan Bowen FBCS FRSAChair BCS-FACS Specialist GroupEmeritus Professor of Computing, London South Bank University
Chairman, Museophile Limited