LEADER 04473nam 22007695 450 001 9910483880903321 005 20220920141503.0 010 $a3-319-49812-6 024 7 $a10.1007/978-3-319-49812-6 035 $a(CKB)3710000001006507 035 $a(DE-He213)978-3-319-49812-6 035 $a(MiAaPQ)EBC6294738 035 $a(MiAaPQ)EBC5576381 035 $a(Au-PeEL)EBL5576381 035 $a(OCoLC)968301788 035 $a(PPN)19745514X 035 $a(EXLCZ)993710000001006507 100 $a20161220d2016 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aDeductive Software Verification ? The KeY Book $eFrom Theory to Practice /$fedited by Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, Mattias Ulbrich 205 $a1st ed. 2016. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2016. 215 $a1 online resource (XXXII, 702 p. 110 illus.) 225 1 $aProgramming and Software Engineering ;$v10001 311 $a3-319-49811-8 320 $aIncludes bibliographical references and index. 327 $aFoundations -- Specification and Verification -- From Verification to Analysis -- The KeY System in Action -- Case Studies. 330 $aStatic 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. 410 0$aProgramming and Software Engineering ;$v10001 606 $aSoftware engineering 606 $aComputer logic 606 $aMathematical logic 606 $aProgramming languages (Electronic computers) 606 $aArtificial intelligence 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 615 0$aSoftware engineering. 615 0$aComputer logic. 615 0$aMathematical logic. 615 0$aProgramming languages (Electronic computers). 615 0$aArtificial intelligence. 615 14$aSoftware Engineering. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Formal Languages. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aArtificial Intelligence. 676 $a005.14 702 $aAhrendt$b Wolfgang$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aBeckert$b Bernhard$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aBubel$b Richard$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aHähnle$b Reiner$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSchmitt$b Peter H$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aUlbrich$b Mattias$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483880903321 996 $aDeductive Software Verification ? The KeY Book$92809759 997 $aUNINA