@book{KeYBook2016, editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H\"ahnle and Peter H. Schmitt and Mattias Ulbrich}, title = {Deductive Software Verification - The {\KeY} Book: From Theory to Practice}, series = {Lecture Notes in Computer Science}, volume = {10001}, publisher = {Springer}, url = {http://dx.doi.org/10.1007/978-3-319-49812-6}, doi = {10.1007/978-3-319-49812-6}, year = {2016}, abstract = {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 {\KeY}. \newline This book is the definitive guide to {\KeY} that lets you explore the full potential of deductive software verification in practice. It contains the complete theory behind {\KeY} 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 {\KeY} that require nothing else than familiarity with Java. All other chapters are accessible for graduate students (M.Sc. level and beyond). \newline The {\KeY} framework is free and open software, downloadable from the book companion website which contains also all code examples mentioned in this book.} }