Just in time for the holiday season, the new book has arrived.
The LNCS volume 12345* “Deductive Software Verification: Future Perspectives” contains a collection of articles – reflections on the occasion of 20 years of KeY.
An account of the history of KeY is contained amongst a collection of articles on Verification Tools, Contracts, the Feasibility and Usability and Integration of Verification Techniques. The articles have been written by leading experts in the field and are not necessarily directly concerned with the KeY verification tool. They give insights to future perspectives in deductive software verification.
The book is now available at Springer.
Many thanks to all authors for their high-quality contributions!
____________
* No! 12345 is not a placeholder number. It is the actual number of the volume. Pretty cool, isn’t it.
Table of Contents
History
- A Short History of KeY by Peter H. Schmitt
Verification Tools
- A Retrospective on Developing Hybrid System Provers in the KeYmaera Family: A Tale of Three Provers by Stefan Mitsch and André Platzer
- Improving Performance of the VerCors Program Verifier by Henk Mulder, Marieke Huisman, and Sebastiaan Joosten
Contracts
- Behavioral Contracts for Cooperative Scheduling by Eduard Kamburjan, Crystal Chang Din, Reiner Hähnle, and Einar Broch Johnsen
- Using Abstract Contracts for Verifying Evolving Features and Their Interactions by Alexander Knüppel, Stefan Krüger, Thomas Thüm, Richard Bubel, Sebastian Krieter, Eric Bodden, and Ina Schaefer
- Constraint-Based Contract Inference for Deductive Verification by Anoud Alshnakat, Dilian Gurov, Christian Lidström, and Philipp Rümmer
- From Explicit to Implicit Dynamic Frames in Concurrent Reasoning for Java by Wojciech Mostowski
- Formal Analysis of Smart Contracts: Applying the KeY System by Jonas Schiffl, Wolfgang Ahrendt, Bernhard Beckert, and Richard Bubel
Feasibility and Usablility
- A Tutorial on Verifying LinkedList Using KeY by Hans-Dieter A. Hiep, Jinting Bian, Frank S. de Boer, and Stijn de Gouw
- The VerifyThis Collaborative Long Term Challenge by Marieke Huisman, Raúl Monti, Mattias Ulbrich, and Alexander Weigl
- Usability Recommendations for User Guidance in Deductive Program Verification by Sarah Grebing and Mattias Ulbrich
Integration of Verification Techniques
- Integration of Static and Dynamic Analysis Techniques for Checking Noninterference by Bernhard Beckert, Mihai Herda, Michael Kirsten, and Shmuel Tyszberowicz
- SymPaths: Symbolic Execution Meets Partial Order Reduction by Frank S. de Boer, Marcello Bonsangue, Einar Broch Johnsen, Violet Ka I Pun, S. Lizeth Tapia Tarifa, and Lars Tveito
