 |
 |
Final reminder for the BCS-FACS/FME evening seminar on Thursday 4 May at the BCS London office, see below. As a slight incentive, we plan to have a light buffet for networking after the talk. There will be a number of FME members from around Europe there too. Do remember to book free online if you wish to attend, so we can get the catering numbers right. -- *Jonathan Bowen* Chair BCS-FACS SG *Prof. Jonathan Bowen <https://sites.google.com/site/jpbowen/> *FBCS FRSA Emeritus Professor of Computing, London South Bank University Chairman, Museophile Limited See *The Turing Guide <http://formalmethods.wikia.com/wiki/The_Turing_Guide>*, Oxford University Press, 2017 On 24 April 2017 at 19:15, Jonathan Bowen <[log in to unmask]> wrote: > *The KeY Formal Verification Tool* > > http://www.bcs.org/content/ConWebDoc/57115 > (Jointly with Formal Methods Europe <http://www.fmeurope.org/> - 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 | Maps <http://www.bcs.org/category/5843> > > *Speaker:* > Prof. Dr. Reiner Hähnle > <https://www.se.tu-darmstadt.de/se/group-members/reiner-haehnle/>, TU > Darmstadt, Germany > *https://www.se.tu-darmstadt.de/se/group-members/reiner-haehnle/ > <https://www.se.tu-darmstadt.de/se/group-members/reiner-haehnle/>* > > *Cost:* > Free > > *Book Online* *https://events.bcs.org/book/2357/ > <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 <https://sites.google.com/site/jpbowen/> *FBCS FRSA > Chair BCS-FACS Specialist Group > Emeritus Professor of Computing, London South Bank University > Chairman, Museophile Limited > See *The Turing Guide > <http://formalmethods.wikia.com/wiki/The_Turing_Guide>*, Oxford > University Press, 2017 > >