KeY - A Deductive Software Analysis Tool for the Research Community

KeY - 面向研究界的演绎软件分析工具

• 批准号: 443187992
• 负责人: Professor Dr. Bernhard Beckert
• 金额: --
• 依托单位: Institut für Theoretische Informatik (ITI)
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/443187992?language=en
• 关键词: KeY; Deductive; Software; Analysis; Tool

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.

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