SHF: Small: Relational Parametricity for Program Verification

职务名称：SHF：小号：软件市场目前估计每年有5000亿美元，随着软件变得越来越普遍，这个数字在真实的方面可能会显著增长。软件的一个关键方面是它是正确的，即，这个软件做了预期的事情，不会出错。即使是iPod和移动的手机等日常设备的故障也会带来不便和沮丧，但软件泄露信用卡详细信息或投票记录、导致飞机坠毁、未经授权发射核武器或危及全球金融部门都可能导致前所未有的、显然不可接受的全球不确定性。不断增长的规模和复杂的程序使得形式验证方法-使用数学技术来确保程序实际执行它们设计执行的计算，而不是执行非预期的计算-对于构建真正安全可靠的软件越来越重要。更广泛的影响，这项研究是使更好的和更广泛适用的形式化程序验证方法的发展成为可能，从而，以帮助确保即使是大型和复杂的软件系统是可证明的correct.Relational parametricity是一个关键技术，正式验证软件系统的属性。逻辑关系是关系参数化的基础，它提供了一种直接从系统本身证明软件系统属性的方法。到目前为止，许多现代编程语言和验证系统的核心片段已经开发出了逻辑关系。然而，这是通过大量复杂和不可重用的逻辑关系来实现的，而不是通过呼吁它们的统一构造和从基本原则的可转移发展。本研究的目的是通过提供一个公理化的逻辑关系构建框架来改进当前的最新技术。该框架是原则性的，概念简单，全面，统一和预测。这项研究的智力价值在于它的阐述和使用的基本结构，从范畴理论（“纤维化”），以解决重大的技术问题，构建逻辑关系，并在复杂的设置概念化的关系参数。它还在于新的和统一的配方参数，这项研究将导致，并应用这个新的框架，以具体的国家的最先进的计算问题。为确保新框架得到采纳，将为新框架提供逻辑和工具支持。虽然该工具将允许用户对框架进行试验，但其实际经验的反馈将进一步加强参数化的新基础。

Title: SHF: Small: Relational Parametricity for Program VerificationThe software market is currently estimated at $500 billion per year, and this figure is likely to grow significantly in real terms as software becomes ever more ubiquitous. One crucial aspect of software is that it be correct, i.e., that software does what's intended and does not go wrong. Even failures of everyday devices like iPods and mobile phones are inconvenient and frustrating, but software leaking credit card details or voting records, causing an airplane to crash, launching nuclear weapons without authorization, or compromising the global financial sector can lead to unprecedented and clearly unacceptable global uncertainties. The ever-growing size and sophistication of programs makes formal verification methods --- which use mathematical techniques to ensure that programs actually perform the computations they are designed to carry out and do not perform unintended ones --- increasingly critical for building truly secure and reliable software. The broader impact of this research is to make possible the development of better and more widely applicable formal program verification methods, and, thereby, to help ensure that even large and sophisticated software systems are provably correct.Relational parametricity is a key technique for formally verifying properties of software systems. Logical relations, upon which relational parametricity is based, provide a means of proving properties of a software system directly from the system itself. Logical relations have by now been developed for core fragments of many modern programming languages and verification systems. However, this has been accomplished by way of an enormous constellation of complicated and non-reusable logical relations, rather than by appealing to their uniform construction and transferrable development from fundamental principles. This research aims to improve the current state-of-the-art by providing an axiomatic framework for the construction of logical relations. The framework is principled, conceptually simple, comprehensive, uniform, and predictive. The intellectual merit of this research lies in its exposition and use of essential structures from category theory ("fibrations") to address the significant technical problems of constructing logical relations, and conceptualizing relational parametricity in sophisticated settings. It also lies in the novel and uniform formulation of parametricity to which this research will lead, and the application of this new framework to specific state-of-the-art computational problems. To ensure its uptake, a logic and tool support for the new framework will be provided. While the tool will permit users to experiment with the framework, the feedback from their practical experiences will further fortify the new foundations for parametricity.