jStar: making java verification practical

软件是不可靠的。这是现代社会的一个严重问题。我们每天都在接触软件，但这些软件经常包含严重的错误。目前，操作系统很容易受到病毒的影响，商业软件包出售时带有免责声明而不是保证。为了解决这个问题，我们需要为现实世界的编程语言开发实用的验证方法。这是关于给出软件应该做什么的数学规范，并保证实现符合该规范。这个建议的重点是验证面向对象的程序。最突出的面向对象验证方法Boogie和ESC存在两个主要问题。首先，它们的规范是冗长的，实际上有时比代码还要长。这样做的原因是它们只支持有限的模块化，并且需要冗余的注释，就像许多循环不变量一样。其次，它们的规范很弱，因为它们不能表达功能的正确性。这里的问题是，尽管“少说多做”的咒语在软件规范的上下文中很有吸引力，但不幸的是，它并不适用于现实的示例，甚至不适用于常见的设计模式。在这里，我们提出了以下新颖的思想组合，使Java的实际验证成为可能：*面向对象的基于分离逻辑的规范语言，提供强大的模块化。*子结构逻辑的自动定理证明，它集成了经典逻辑的现有定理证明，例如SMT求解器；假日;*一种抽象解释的证明理论方法，它允许推断冗余的注释，并将抽象解释提高到覆盖完整的功能正确性属性。此外，我们建议所有这些概念可以在一个统一的证明者/抽象者体系结构中一起实现。

Software is unreliable. This is a serious problem for modern society. We are in contact with software everyday, but this software often contains critical bugs. Currently, operating systems are susceptible to viruses, and commercial software packages are sold with disclaimers not guarantees. To address this, we need to develop practical verfication methods for real-world programming languages. This is about giving a mathematical specification of what the software should do, and guaranteeing the implementation meets this specification. This proposal focusses on verifying object-oriented programs. The most prominent approaches to object-oriented verification, Boogie and ESC, suffer two major problems. First, their specifications are verbose, in fact sometimes longer than the code. The reason for this is that they only support limited modularity and require redundant annotations, like many loop invariants. Secondly, their specifications are weak since they cannot express functional correctness. The problem here is that although the mantra ``say less to do more'' is alluring in the context of software specification, unfortunately, it does not work for realistic examples, or even just common design patterns. Here, we propose the following novel combination of ideas, which make practical verification for Java possible: * A separation Logic based specification language for OO giving powerful modularity. * Automatic theorem proving for substructural logics which integrates with existing theorem provers for classical logic, e.g. SMT solvers; HOL; etc. * A proof theoretic approach to abstract interpretation, which allows redundant annotations to be inferred and boost abstract interpretation to coverage of full functional correctness properties. Furthermore, we propose that all these concepts can be realised together in a unified prover/abstracter architecture.