KeY - A Deductive Software Analysis Tool for the Research Community

点击翻译按钮获取中文摘要

Computer Science is the key science behind the ongoing digital revolution and thus became a foundational science. At the core of the digital paradigm shift is the ability to specify, to produce, to understand, and to maintain high-quality, reliable software. Researchers (computer scientists together with domain experts) must be enabled to manifest trust in their own software. One way to obtain this trust is by the application of formal analysis tools that yield mathematically rigorous guarantees.The KeY System is a state-of-art static analysis tool for one of the most popular programming languages: Java. KeY is open source and published under the GPL license.KeY allows one to formally specify and verify Java code. In addition, KeY can generate test cases with high code coverage and visualize symbolic execution trees for program understanding and debugging.The main goal of this project is to make KeY so usable and robust that it can be successfully applied by computer science researchers outside the KeY team.We provide KeY as a test bed for experiments in the area of formal methods, and as a platform for implementing new approaches and methods for ensuring and analysing the reliability of research software. Because the ongoing shift from physical implements to software in all fields of research, it is now software that has to carry part of the trust in scientific results. In this sense, research software is trust-critical.We target researchers working with Computer Science methods to improve software techniques (evolution, development, dependability, security), possibly in application domains. This could be computer scientists in a CS department or - as it is increasingly common - computer scientists working on software development in different research fields.The work is pursued in three technical areas: (i) to improve the User Experience by improving accessibility, eliminate need for expertise, and establish a closed design-experiment-analyse-adapt research cycle supported by automation; (ii) to establish Robustness so that KeY works out of the box for simpler problems, does not crash when fed with ones it cannot solve, and gives good error messages in this case; (iii) prepare support for Adaptation to other source code languages than Java. These technical areas are complemented by a fourth area on Coordination with non-technical work packages on infrastructure, documentation, community support.The project provides the ground to establish an active research community around KeY. Building a community is crucial to provide sustainable resources beyond the runtime of this project for keeping the platform up-to-date and to keep pace with the integration of new language features in the supported target programming languages.