Deductive Software Verification: Future Perspectives Reflections on the Occasion of 20 Years of KeY /
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 t...
| Corporate Author: | |
|---|---|
| Other Authors: | , , , , |
| Language: | English |
| Published: |
Cham :
Springer International Publishing : Imprint: Springer,
2020.
|
| Edition: | 1st ed. 2020. |
| Series: | Programming and Software Engineering ;
12345 |
| Subjects: | |
| Online Access: | https://doi.org/10.1007/978-3-030-64354-6 |
Table of Contents:
- 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.