Editors:
- Unique visibility
- Integrates classic material and new concepts
- Written by experts
- Includes supplementary material: sn.pub/extras
Part of the book series: Lecture Notes in Computer Science (LNCS, volume 10001)
Part of the book sub series: Programming and Software Engineering (LNPSE)
Buy it now
Buying options
Tax calculation will be finalised at checkout
Other ways to access
This is a preview of subscription content, log in via an institution to check for access.
Table of contents (19 chapters)
-
Front Matter
-
Foundations
-
Front Matter
-
-
Specification and Verification
-
Front Matter
-
-
From Verification to Analysis
-
Front Matter
-
-
The KeY System in Action
-
Front Matter
-
About this book
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.
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).
The KeY framework is free and open software, downloadable from the book companion website which contains also all code examples mentioned in this book.
Keywords
- deductive verification
- first-order logic
- formal methods
- semantic constraints
- software development
- case studies
- compilation
- debugging tool
- formal software analysis
- formal specification
- formal verification
- integer semantics
- partial evaluation
- program transformation
- programming language
- specification language
- symbolic execution
- test case generation
- visualization
Editors and Affiliations
-
Chalmers University of Technology, Gothenburg, Sweden
Wolfgang Ahrendt
-
Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany
Bernhard Beckert
-
Technische Universität Darmstadt, Darmstadt, Germany
Richard Bubel, Reiner Hähnle
-
Karlsruher Institut für Technologie (KIT), Karlsruhe, Germany
Peter H. Schmitt, Mattias Ulbrich
Bibliographic Information
Book Title: Deductive Software Verification – The KeY Book
Book Subtitle: From Theory to Practice
Editors: Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, Mattias Ulbrich
Series Title: Lecture Notes in Computer Science
DOI: https://doi.org/10.1007/978-3-319-49812-6
Publisher: Springer Cham
eBook Packages: Computer Science, Computer Science (R0)
Copyright Information: Springer International Publishing AG 2016
Softcover ISBN: 978-3-319-49811-9Published: 21 December 2016
eBook ISBN: 978-3-319-49812-6Published: 19 December 2016
Series ISSN: 0302-9743
Series E-ISSN: 1611-3349
Edition Number: 1
Number of Pages: XXXII, 702
Number of Illustrations: 110 b/w illustrations
Topics: Software Engineering, Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Programming Languages, Compilers, Interpreters, Artificial Intelligence