KeY - A Deductive Software Analysis Tool for the Research Community

计算机科学是正在进行的数字革命背后的关键科学，因此成为基础科学。数字范式转变的核心是指定、生产、理解和维护高质量、可靠的软件的能力。 研究人员（计算机科学家和领域专家）必须能够在他们自己的软件中表现出信任。获得这种信任的一种方法是应用形式化分析工具，这些工具可以产生数学上严格的保证。KeY System是最流行的编程语言之一Java的最先进的静态分析工具。KeY是开源的，并在GPL许可证下发布。KeY允许正式指定和验证Java代码。此外，KeY还可以生成高代码覆盖率的测试用例，并可视化符号执行树，用于程序理解和调试。本项目的主要目标是使KeY变得可用和健壮，以便KeY团队以外的计算机科学研究人员能够成功地应用它。我们提供KeY作为形式化方法领域实验的测试床，并作为一个平台，实施新的途径和方法，以确保和分析研究软件的可靠性。 由于所有研究领域都在不断从物理工具转向软件，现在软件必须承载对科学成果的部分信任。从这个意义上说，研究软件是信任关键的。我们的目标是研究人员与计算机科学的方法，以改善软件技术（进化，开发，可靠性，安全性），可能在应用领域。这可能是计算机科学部门的计算机科学家，或者是越来越常见的在不同研究领域从事软件开发的计算机科学家。这项工作在三个技术领域进行：（i）通过提高可访问性来改善用户体验，消除对专业知识的需求，并建立一个由自动化支持的封闭的设计-实验-分析-适应研究周期;（ii）建立健壮性，使KeY能够开箱即用地解决更简单的问题，当输入无法解决的问题时不会崩溃，并在这种情况下给出良好的错误信息;（iii）准备支持适应Java以外的其他源代码语言。 这些技术领域由第四个领域补充，即与基础设施、文献、社区支持等非技术工作包协调。该项目为围绕KeY建立一个活跃的研究社区奠定了基础。构建社区对于在项目运行时之外提供可持续的资源至关重要，以保持平台最新，并跟上支持的目标编程语言中新语言功能的集成。

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.