Deductive Software Verification – The KeY Book 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, visuali...

Full description

Corporate Author: SpringerLink (Online service)
Other Authors: Ahrendt, Wolfgang. (Editor, http://id.loc.gov/vocabulary/relators/edt), Beckert, Bernhard. (Editor, http://id.loc.gov/vocabulary/relators/edt), Bubel, Richard. (Editor, http://id.loc.gov/vocabulary/relators/edt), Hähnle, Reiner. (Editor, http://id.loc.gov/vocabulary/relators/edt), Schmitt, Peter H. (Editor, http://id.loc.gov/vocabulary/relators/edt), Ulbrich, Mattias. (Editor, http://id.loc.gov/vocabulary/relators/edt)
Language:English
Published: Cham : Springer International Publishing : Imprint: Springer, 2016.
Edition:1st ed. 2016.
Series:Programming and Software Engineering ; 10001
Subjects:
Online Access:https://doi.org/10.1007/978-3-319-49812-6
LEADER 04211nam a22006255i 4500
001 978-3-319-49812-6
003 DE-He213
005 20210624235612.0
007 cr nn 008mamaa
008 161220s2016 gw | s |||| 0|eng d
020 |a 9783319498126  |9 978-3-319-49812-6 
024 7 |a 10.1007/978-3-319-49812-6  |2 doi 
050 4 |a QA76.758 
072 7 |a UMZ  |2 bicssc 
072 7 |a COM051230  |2 bisacsh 
072 7 |a UMZ  |2 thema 
082 0 4 |a 005.1  |2 23 
245 1 0 |a Deductive Software Verification – The KeY Book  |h [electronic resource] :  |b From Theory to Practice /  |c edited by Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, Mattias Ulbrich. 
250 |a 1st ed. 2016. 
264 1 |a Cham :  |b Springer International Publishing :  |b Imprint: Springer,  |c 2016. 
300 |a XXXII, 702 p. 110 illus.  |b online resource. 
336 |a text  |b txt  |2 rdacontent 
337 |a computer  |b c  |2 rdamedia 
338 |a online resource  |b cr  |2 rdacarrier 
347 |a text file  |b PDF  |2 rda 
490 1 |a Programming and Software Engineering ;  |v 10001 
505 0 |a Foundations -- Specification and Verification -- From Verification to Analysis -- The KeY System in Action -- Case Studies. 
520 |a 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. 
650 0 |a Software engineering. 
650 0 |a Computer logic. 
650 0 |a Mathematical logic. 
650 0 |a Programming languages (Electronic computers). 
650 0 |a Artificial intelligence. 
650 1 4 |a Software Engineering.  |0 https://scigraph.springernature.com/ontologies/product-market-codes/I14029 
650 2 4 |a Logics and Meanings of Programs.  |0 https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 
650 2 4 |a Mathematical Logic and Formal Languages.  |0 https://scigraph.springernature.com/ontologies/product-market-codes/I16048 
650 2 4 |a Programming Languages, Compilers, Interpreters.  |0 https://scigraph.springernature.com/ontologies/product-market-codes/I14037 
650 2 4 |a Artificial Intelligence.  |0 https://scigraph.springernature.com/ontologies/product-market-codes/I21000 
700 1 |a Ahrendt, Wolfgang.  |e editor.  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
700 1 |a Beckert, Bernhard.  |e editor.  |0 (orcid)0000-0002-9672-3291  |1 https://orcid.org/0000-0002-9672-3291  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
700 1 |a Bubel, Richard.  |e editor.  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
700 1 |a Hähnle, Reiner.  |e editor.  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
700 1 |a Schmitt, Peter H.  |e editor.  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
700 1 |a Ulbrich, Mattias.  |e editor.  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
710 2 |a SpringerLink (Online service) 
773 0 |t Springer Nature eBook 
776 0 8 |i Printed edition:  |z 9783319498119 
776 0 8 |i Printed edition:  |z 9783319498133 
830 0 |a Programming and Software Engineering ;  |v 10001 
856 4 0 |u https://doi.org/10.1007/978-3-319-49812-6 
912 |a ZDB-2-SCS 
912 |a ZDB-2-SXCS 
912 |a ZDB-2-LNC 
950 |a Computer Science (SpringerNature-11645) 
950 |a Computer Science (R0) (SpringerNature-43710)