000958954 000__ 04546cam\a2200601Ii\4500
000958954 001__ 958954
000958954 005__ 20230306152629.0
000958954 006__ m\\\\\o\\d\\\\\\\\
000958954 007__ cr\nn\nnnunnun
000958954 008__ 201208s2020\\\\sz\a\\\\o\\\\\001\0\eng\d
000958954 019__ $$a1226586972$$a1227395265$$a1228843555$$a1233068943
000958954 020__ $$a9783030643546$$q(electronic book)
000958954 020__ $$a3030643549$$q(electronic book)
000958954 020__ $$z9783030643539
000958954 0247_ $$a10.1007/978-3-030-64354-6$$2doi
000958954 035__ $$aSP(OCoLC)on1228649515
000958954 035__ $$aSP(OCoLC)1228649515$$z(OCoLC)1226586972$$z(OCoLC)1227395265$$z(OCoLC)1228843555$$z(OCoLC)1233068943
000958954 040__ $$aSFB$$beng$$erda$$cSFB$$dOCLCO$$dOCLCF$$dGW5XE$$dEBLCP$$dUPM$$dUKBTH$$dOCLCO
000958954 049__ $$aISEA
000958954 050_4 $$aQA76.76.V47
000958954 08204 $$a005.1/4$$223
000958954 24500 $$aDeductive software verification: future perspectives :$$breflections on the occasion of 20 years of KeY /$$cWolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Mattias Ulbrich (eds.).
000958954 264_1 $$aCham :$$bSpringer,$$c[2020]
000958954 300__ $$a1 online resource (xii, 339 pages) :$$billustrations (some color).
000958954 336__ $$atext$$btxt$$2rdacontent
000958954 337__ $$acomputer$$bc$$2rdamedia
000958954 338__ $$aonline resource$$bcr$$2rdacarrier
000958954 347__ $$atext file
000958954 347__ $$bPDF
000958954 4901_ $$aLecture notes in computer science ;$$v12345
000958954 4901_ $$aLNCS sublibrary: SL2. Programming and software engineering
000958954 500__ $$aIncludes author index.
000958954 5050_ $$aHistory -- A Short History of KeY -- Verification Tools -- A Retrospective on Developing Hybrid System Provers in the KeYmaera Family - A Tale of Three Provers -- Improving Performance of the VerCors Program Verifier -- Contracts -- Behavioral Contracts for Cooperative Scheduling -- Using Abstract Contracts for Verifying Evolving Features and Their Interactions -- Constraint-based Contract Inference for Deductive Verification -- From Explicit to Implicit Dynamic Frames in Concurrent Reasoning for Java -- Feasibility and Usability -- A Tutorial on Verifying LinkedList Using KeY -- The VerifyThis Collaborative Long Term Challenge -- Usability Recommendations for User Guidance in Deductive Program Verification -- Integration of Verification Techniques -- Integration of Static and Dynamic Analysis Techniques for Checking Noninterference -- SymPaths: Symbolic Execution Meets Partial Order Reduction.
000958954 506__ $$aAccess limited to authorized users.
000958954 520__ $$aSince the inception of the KeY project two decades ago, the area of deductive verification has evolved considerably. Support for real world programming languages by deductive program verification tools has become prevalent. This required to overcome significant theoretical and technical challenges to support advanced software engineering and programming concepts. The community became more interconnected with a competitive, but friendly and supportive environment. We took the 20 year anniversary of KeY as an opportunity to invite researchers, inside and outside of the project, to contribute to a book capturing some state-of-the-art developments in the field. We received thirteen contributions from recognized experts of the field addressing the latest challenges. The topics of the contributions range from tool development, effciency and usability considerations to novel specification and verification methods. This book should offer the reader an up-to-date impression of the current state-of-art in deductive verification, and we hope, inspire her to contribute to the field and to join forces. We are looking forward to meeting you at the next conference, to listen to your research talks and the resulting fruitful discussions and collaborations.
000958954 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed February 16, 2021).
000958954 650_0 $$aComputer software$$xVerification.
000958954 650_0 $$aSoftware engineering.
000958954 650_0 $$aComputer logic.
000958954 650_0 $$aArtificial intelligence.
000958954 650_0 $$aApplication software.
000958954 7001_ $$aAhrendt, Wolfgang,$$eeditor.
000958954 7001_ $$aBeckert, Bernhard,$$eeditor.
000958954 7001_ $$aBubel, Richard,$$eeditor.
000958954 7001_ $$aHähnle, Reiner,$$eeditor.
000958954 7001_ $$aUlbrich, Mattias,$$eeditor.
000958954 77608 $$z3030643530
000958954 830_0 $$aLecture notes in computer science ;$$v12345.
000958954 830_0 $$aLNCS sublibrary.$$nSL 2,$$pProgramming and software engineering.
000958954 852__ $$bebk
000958954 85640 $$3SpringerLink$$uhttps://univsouthin.idm.oclc.org/login?url=http://link.springer.com/10.1007/978-3-030-64354-6$$zOnline Access$$91397441.1
000958954 909CO $$ooai:library.usi.edu:958954$$pGLOBAL_SET
000958954 980__ $$aEBOOK
000958954 980__ $$aBIB
000958954 982__ $$aEbook
000958954 983__ $$aOnline
000958954 994__ $$a92$$bISE