國立高雄大學圖資館 |

Language: English

Back

Deductive software verificationfutur...

Ahrendt, Wolfgang.

Deductive software verificationfuture perspectives : reflections on the occasion of 20 years of KeY /

Record Type:	Electronic resources : Monograph/item
Title/Author:	Deductive software verificationedited by Wolfgang Ahrendt ... [et al.].
Reminder of title:	future perspectives : reflections on the occasion of 20 years of KeY /
other author:	Ahrendt, Wolfgang.
Published:	Cham :Springer International Publishing :2020.
Description:	xii, 339 p. :ill. (some col.), digital ;24 cm.
Contained By:	Springer Nature eBook
Subject:	Computer softwareVerification.
Online resource:	https://doi.org/10.1007/978-3-030-64354-6
ISBN:	9783030643546$q(electronic bk.)

Deductive software verificationfuture perspectives : reflections on the occasion of 20 years of KeY /
Deductive software verificationfuture perspectives : reflections on the occasion of 20 years of KeY /[electronic resource] :edited by Wolfgang Ahrendt ... [et al.]. - Cham :Springer International Publishing :2020. - xii, 339 p. :ill. (some col.), digital ;24 cm. - Lecture notes in computer science,123450302-9743 ;. - Lecture notes in computer science ;4891..

History -- 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.

Since 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.

ISBN: 9783030643546$q(electronic bk.)

Standard No.: 10.1007/978-3-030-64354-6doiSubjects--Topical Terms:

184731
Computer software
--Verification.

LC Class. No.: QA76.76.V47

Dewey Class. No.: 005.14

Deductive software verificationfuture perspectives : reflections on the occasion of 20 years of KeY /
LDR:03369nmm a2200361 a 4500 001 591409
003 DE-He213
005 20201208112417.0
006 m d
007 cr nn 008maaau
008 210629s2020 sz s 0 eng d
020 $a 9783030643546$q(electronic bk.)
020 $a 9783030643539$q(paper)
024 7 $a 10.1007/978-3-030-64354-6 $2 doi
035 $a 978-3-030-64354-6
040 $a GP $c GP
041 0 $a eng
050 4 $a QA76.76.V47
072 7 $a UMZ $2 bicssc
072 7 $a COM051230 $2 bisacsh
072 7 $a UMZ $2 thema
072 7 $a UL $2 thema
082 0 4 $a 005.14 $2 23
090 $a QA76.76.V47 $b D299 2020
245 0 0 $a Deductive software verification $h [electronic resource] : $b future perspectives : reflections on the occasion of 20 years of KeY / $c edited by Wolfgang Ahrendt ... [et al.].
260 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2020.
300 $a xii, 339 p. : $b ill. (some col.), digital ; $c 24 cm.
490 1 $a Lecture notes in computer science, $x 0302-9743 ; $v 12345
490 1 $a Programming and software engineering
505 0 $a History -- 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.
520 $a Since 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.
650 0 $a Computer software $x Verification. $3 184731
650 1 4 $a Software Engineering/Programming and Operating Systems. $3 273711
650 2 4 $a Logics and Meanings of Programs. $3 275357
650 2 4 $a Artificial Intelligence. $3 212515
650 2 4 $a Information Systems Applications (incl. Internet) $3 530743
700 1 $a Ahrendt, Wolfgang. $3 764266
710 2 $a SpringerLink (Online service) $3 273601
773 0 $t Springer Nature eBook
830 0 $a Lecture notes in computer science ; $v 4891. $3 383229
830 0 $a Programming and software engineering. $3 821998
856 4 0 $u https://doi.org/10.1007/978-3-030-64354-6
950 $a Computer Science (SpringerNature-11645)