Wolfgang Ahrendt & Bernhard Beckert 
Deductive Software Verification — The KeY Book [PDF ebook] 
From Theory to Practice

Static analysis of software with deductive methods is a highly dynamic field of research on the verge of becoming a mainstream technology in software engineering. It consists of a large portfolio of — mostly fully automated — analyses: formal verification, test generation, security analysis, visualization, and debugging. All of them are realized in the state-of-art deductive verification framework Ke Y.This book is the definitive guide to Ke Y that lets you explore the full potential of deductive software verification in practice. It contains the complete theory behind Ke Y for active researchers who want to understand it in depth or use it in their own work. But the book also features fully self-contained chapters on the Java Modeling Language and on Using Ke Y that require nothing else than familiarity with Java. All other chapters are accessible for graduate students (M.Sc. level and beyond). The Ke Y framework is free and open software, downloadable from the book companion website which contains also all code examples mentioned in this book.